# HG changeset patch
# User haftmann
# Date 1217396035 -7200
# Node ID f6277c8ab8ef472569ab048aec0defadbbc2dac5
# Parent  5b1585b489527012cdaa741d10e6a55532052b50
tuned

diff -r 5b1585b48952 -r f6277c8ab8ef doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy
--- a/doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy	Tue Jul 29 17:50:48 2008 +0200
+++ b/doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy	Wed Jul 30 07:33:55 2008 +0200
@@ -315,7 +315,7 @@
   equation, using the \emph{func del} attribute:
 *}
 
-lemmas [code func del] = pick.simps 
+declare pick.simps [code func del]
 
 export_code pick (*<*)in SML(*>*) in SML file "examples/pick2.ML"
 
@@ -506,7 +506,7 @@
 
   The \emph{simpset} allows to employ the full generality of the Isabelle
   simplifier.  Due to the interpretation of theorems
-  of defining equations, rewrites are applied to the right
+  as defining equations, rewrites are applied to the right
   hand side and the arguments of the left hand side of an
   equation, but never to the constant heading the left hand side.
   An important special case are \emph{inline theorems} which may be
@@ -551,7 +551,7 @@
   list of function theorems, provided that neither the heading
   constant nor its type change.  The @{term "0\<Colon>nat"} / @{const Suc}
   pattern elimination implemented in
-  theory @{text "Efficient_Nat"} (\secref{eff_nat}) uses this
+  theory @{text "Efficient_Nat"} (see \secref{eff_nat}) uses this
   interface.
 
   \noindent The current setup of the preprocessor may be inspected using
@@ -752,7 +752,7 @@
   extend this table;  as an example, we will develope an alternative
   representation of natural numbers as binary digits, whose
   size does increase logarithmically with its value, not linear
-  \footnote{Indeed, the @{text "Efficient_Nat"} theory \ref{eff_nat}
+  \footnote{Indeed, the @{text "Efficient_Nat"} theory (see \ref{eff_nat})
     does something similar}.  First, the digit representation:
 *}
 
@@ -1015,7 +1015,7 @@
   pretty serializations for expressions like lists, numerals
   and characters;  these are
   monolithic stubs and should only be used with the
-  theories introduces in \secref{sec:library}.
+  theories introduced in \secref{sec:library}.
 *}