Wed, 30 Jul 2008 07:33:55 +0200
changeset 27705 f6277c8ab8ef
parent 27704 5b1585b48952
child 27706 10a6ede68bc8
--- 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
   \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}.