# HG changeset patch
# User haftmann
# Date 1180552151 -7200
# Node ID cf50eb79d107b2e1b845398089d173272591625d
# Parent  a318773dca05847aac014d145c0721dd86b3c20a
eliminated strings

diff -r a318773dca05 -r cf50eb79d107 doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy
--- a/doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy	Wed May 30 21:09:09 2007 +0200
+++ b/doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy	Wed May 30 21:09:11 2007 +0200
@@ -133,12 +133,14 @@
 text {*
   \noindent For testing purpose, we define a small example
   using natural numbers @{typ nat} (which are a @{text linorder})
-  as keys and strings values:
+  as keys and list of nats as values:
 *}
 
-fun
-  example :: "nat \<Rightarrow> (nat, string) searchtree" where
-  "example n = update (n, ''bar'') (Leaf 0 ''foo'')"
+definition
+  example :: "(nat, nat list) searchtree"
+where
+  "example = update (Suc (Suc (Suc (Suc 0))), [Suc (Suc 0), Suc (Suc 0)]) (update (Suc (Suc (Suc 0)), [Suc (Suc (Suc 0))])
+    (update (Suc (Suc 0), [Suc (Suc 0)]) (Leaf (Suc 0) [])))"
 
 text {*
   \noindent Then we generate code
@@ -686,10 +688,11 @@
   In some cases, the automatically derived defining equations
   for equality on a particular type may not be appropriate.
   As example, watch the following datatype representing
-  monomorphic parametric types:
+  monomorphic parametric types (where type constructors
+  are referred to by natural numbers):
 *}
 
-datatype monotype = Mono string "monotype list"
+datatype monotype = Mono nat "monotype list"
 (*<*)
 lemma monotype_eq:
   "Mono tyco1 typargs1 = Mono tyco2 typargs2 \<equiv> 
@@ -699,9 +702,9 @@
 text {*
   Then code generation for SML would fail with a message
   that the generated code conains illegal mutual dependencies:
-  the theorem @{thm monotype_eq} already requires the
+  the theorem @{thm monotype_eq [no_vars]} already requires the
   instance @{text "monotype \<Colon> eq"}, which itself requires
-  @{thm monotype_eq};  Haskell has no problem with mutually
+  @{thm monotype_eq [no_vars]};  Haskell has no problem with mutually
   recursive @{text instance} and @{text function} definitions,
   but the SML serializer does not support this.
 
@@ -1295,7 +1298,6 @@
 
   \medskip
   \begin{tabular}{l}
-  @{text "val name: string"} \\
   @{text "type T"} \\
   @{text "val empty: T"} \\
   @{text "val merge: Pretty.pp \<rightarrow> T * T \<rightarrow> T"} \\
@@ -1304,8 +1306,6 @@
 
   \begin{description}
 
-  \item @{text name} is a system-wide unique name identifying the data.
-
   \item @{text T} the type of data to store.
 
   \item @{text empty} initial (empty) data.
@@ -1328,7 +1328,6 @@
 
   \medskip
   \begin{tabular}{l}
-  @{text "init: theory \<rightarrow> theory"} \\
   @{text "get: theory \<rightarrow> T"} \\
   @{text "change: theory \<rightarrow> (T \<rightarrow> T) \<rightarrow> T"} \\
   @{text "change_yield: theory \<rightarrow> (T \<rightarrow> 'a * T) \<rightarrow> 'a * T"}
@@ -1336,8 +1335,6 @@
 
   \begin{description}
 
-  \item @{text init} initialization during theory setup.
-
   \item @{text get} retrieval of the current data.
 
   \item @{text change} update of current data (cached!)
@@ -1362,15 +1359,11 @@
 
   \medskip
   \begin{tabular}{l}
-  @{text "val name: string"} \\
   @{text "val rewrites: theory \<rightarrow> thm list"}
   \end{tabular}
 
   \begin{description}
 
-  \item @{text name} is a system-wide unique name identifying
-    this particular system of defining equations.
-
   \item @{text rewrites} specifies a set of theory-dependent
     rewrite rules which are added to the preprocessor setup;
     if no additional preprocessing is required, pass