# HG changeset patch
# User haftmann
# Date 1275319893 -7200
# Node ID b8e02ce2559fd323823eb128a227021c7019b1a4
# Parent  32a6f471f090a305721f51dc057ddedb2cf29b9a
updated generated files

diff -r 32a6f471f090 -r b8e02ce2559f doc-src/Codegen/Thy/document/ML.tex
--- a/doc-src/Codegen/Thy/document/ML.tex	Mon May 31 17:29:28 2010 +0200
+++ b/doc-src/Codegen/Thy/document/ML.tex	Mon May 31 17:31:33 2010 +0200
@@ -60,9 +60,9 @@
 \verb|    -> theory -> theory| \\
   \indexdef{}{ML}{Code\_Preproc.del\_functrans}\verb|Code_Preproc.del_functrans: string -> theory -> theory| \\
   \indexdef{}{ML}{Code.add\_datatype}\verb|Code.add_datatype: (string * typ) list -> theory -> theory| \\
-  \indexdef{}{ML}{Code.get\_datatype}\verb|Code.get_datatype: theory -> string|\isasep\isanewline%
+  \indexdef{}{ML}{Code.get\_type}\verb|Code.get_type: theory -> string|\isasep\isanewline%
 \verb|    -> (string * sort) list * (string * typ list) list| \\
-  \indexdef{}{ML}{Code.get\_datatype\_of\_constr}\verb|Code.get_datatype_of_constr: theory -> string -> string option|
+  \indexdef{}{ML}{Code.get\_type\_of\_constr\_or\_abstr}\verb|Code.get_type_of_constr_or_abstr: theory -> string -> (string * bool) option|
   \end{mldecls}
 
   \begin{description}
@@ -91,7 +91,7 @@
      a datatype to executable content, with generation
      set \isa{cs}.
 
-  \item \verb|Code.get_datatype_of_constr|~\isa{thy}~\isa{const}
+  \item \verb|Code.get_type_of_constr_or_abstr|~\isa{thy}~\isa{const}
      returns type constructor corresponding to
      constructor \isa{const}; returns \isa{NONE}
      if \isa{const} is no constructor.
@@ -163,7 +163,7 @@
   merge, which is a little bit nasty from an implementation
   point of view.  The framework provides a solution
   to this technical challenge by providing a functorial
-  data slot \verb|CodeDataFun|; on instantiation
+  data slot \verb|Code_Data|; on instantiation
   of this functor, the following types and operations
   are required:
 
@@ -189,7 +189,7 @@
 
   \end{description}
 
-  \noindent An instance of \verb|CodeDataFun| provides the following
+  \noindent An instance of \verb|Code_Data| provides the following
   interface:
 
   \medskip
diff -r 32a6f471f090 -r b8e02ce2559f doc-src/Codegen/Thy/document/Program.tex
--- a/doc-src/Codegen/Thy/document/Program.tex	Mon May 31 17:29:28 2010 +0200
+++ b/doc-src/Codegen/Thy/document/Program.tex	Mon May 31 17:31:33 2010 +0200
@@ -432,9 +432,9 @@
 %
 \isatagquote
 \isacommand{lemma}\isamarkupfalse%
-\ {\isacharbrackleft}code{\isacharunderscore}inline{\isacharbrackright}{\isacharcolon}\isanewline
-\ \ {\isachardoublequoteopen}x\ {\isasymin}\ set\ xs\ {\isasymlongleftrightarrow}\ x\ mem\ xs{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
-\ {\isacharparenleft}induct\ xs{\isacharparenright}\ simp{\isacharunderscore}all%
+\ {\isacharbrackleft}code{\isacharunderscore}unfold{\isacharbrackright}{\isacharcolon}\isanewline
+\ \ {\isachardoublequoteopen}x\ {\isasymin}\ set\ xs\ {\isasymlongleftrightarrow}\ member\ xs\ x{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
+\ {\isacharparenleft}fact\ in{\isacharunderscore}set{\isacharunderscore}code{\isacharparenright}%
 \endisatagquote
 {\isafoldquote}%
 %
@@ -453,9 +453,9 @@
 %
 \isatagquote
 \isacommand{lemma}\isamarkupfalse%
-\ {\isacharbrackleft}code{\isacharunderscore}inline{\isacharbrackright}{\isacharcolon}\isanewline
+\ {\isacharbrackleft}code{\isacharunderscore}unfold{\isacharbrackright}{\isacharcolon}\isanewline
 \ \ {\isachardoublequoteopen}{\isadigit{1}}\ {\isacharequal}\ Suc\ {\isadigit{0}}{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
-\ simp%
+\ {\isacharparenleft}fact\ One{\isacharunderscore}nat{\isacharunderscore}def{\isacharparenright}%
 \endisatagquote
 {\isafoldquote}%
 %
@@ -474,9 +474,9 @@
 %
 \isatagquote
 \isacommand{lemma}\isamarkupfalse%
-\ {\isacharbrackleft}code{\isacharunderscore}inline{\isacharbrackright}{\isacharcolon}\isanewline
+\ {\isacharbrackleft}code{\isacharunderscore}unfold{\isacharbrackright}{\isacharcolon}\isanewline
 \ \ {\isachardoublequoteopen}xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymlongleftrightarrow}\ List{\isachardot}null\ xs{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
-\ {\isacharparenleft}induct\ xs{\isacharparenright}\ simp{\isacharunderscore}all%
+\ {\isacharparenleft}fact\ empty{\isacharunderscore}null{\isacharparenright}%
 \endisatagquote
 {\isafoldquote}%
 %
@@ -763,7 +763,7 @@
 %
 \begin{isamarkuptext}%
 \noindent The membership test during preprocessing is rewritten,
-  resulting in \isa{op\ mem}, which itself
+  resulting in \isa{member}, which itself
   performs an explicit equality check.%
 \end{isamarkuptext}%
 \isamarkuptrue%
@@ -781,7 +781,7 @@
 \hspace*{0pt} ~type 'a eq\\
 \hspace*{0pt} ~val eq :~'a eq -> 'a -> 'a -> bool\\
 \hspace*{0pt} ~val eqa :~'a eq -> 'a -> 'a -> bool\\
-\hspace*{0pt} ~val member :~'a eq -> 'a -> 'a list -> bool\\
+\hspace*{0pt} ~val member :~'a eq -> 'a list -> 'a -> bool\\
 \hspace*{0pt} ~val collect{\char95}duplicates :\\
 \hspace*{0pt} ~~~'a eq -> 'a list -> 'a list -> 'a list -> 'a list\\
 \hspace*{0pt}end = struct\\
@@ -791,13 +791,13 @@
 \hspace*{0pt}\\
 \hspace*{0pt}fun eqa A{\char95}~a b = eq A{\char95}~a b;\\
 \hspace*{0pt}\\
-\hspace*{0pt}fun member A{\char95}~x [] = false\\
-\hspace*{0pt} ~| member A{\char95}~x (y ::~ys) = eqa A{\char95}~x y orelse member A{\char95}~x ys;\\
+\hspace*{0pt}fun member A{\char95}~[] y = false\\
+\hspace*{0pt} ~| member A{\char95}~(x ::~xs) y = eqa A{\char95}~x y orelse member A{\char95}~xs y;\\
 \hspace*{0pt}\\
 \hspace*{0pt}fun collect{\char95}duplicates A{\char95}~xs ys [] = xs\\
 \hspace*{0pt} ~| collect{\char95}duplicates A{\char95}~xs ys (z ::~zs) =\\
-\hspace*{0pt} ~~~(if member A{\char95}~z xs\\
-\hspace*{0pt} ~~~~~then (if member A{\char95}~z ys then collect{\char95}duplicates A{\char95}~xs ys zs\\
+\hspace*{0pt} ~~~(if member A{\char95}~xs z\\
+\hspace*{0pt} ~~~~~then (if member A{\char95}~ys z then collect{\char95}duplicates A{\char95}~xs ys zs\\
 \hspace*{0pt} ~~~~~~~~~~~~else collect{\char95}duplicates A{\char95}~xs (z ::~ys) zs)\\
 \hspace*{0pt} ~~~~~else collect{\char95}duplicates A{\char95}~(z ::~xs) (z ::~ys) zs);\\
 \hspace*{0pt}\\
@@ -968,11 +968,10 @@
 \hspace*{0pt}empty{\char95}queue ::~forall a.~a;\\
 \hspace*{0pt}empty{\char95}queue = error {\char34}empty{\char95}queue{\char34};\\
 \hspace*{0pt}\\
-\hspace*{0pt}strict{\char95}dequeue' ::~forall a.~Queue a -> (a,~Queue a);\\
-\hspace*{0pt}strict{\char95}dequeue' (AQueue xs (y :~ys)) = (y,~AQueue xs ys);\\
-\hspace*{0pt}strict{\char95}dequeue' (AQueue xs []) =\\
-\hspace*{0pt} ~(if nulla xs then empty{\char95}queue\\
-\hspace*{0pt} ~~~else strict{\char95}dequeue' (AQueue [] (rev xs)));%
+\hspace*{0pt}strict{\char95}dequeue ::~forall a.~Queue a -> (a,~Queue a);\\
+\hspace*{0pt}strict{\char95}dequeue (AQueue xs (y :~ys)) = (y,~AQueue xs ys);\\
+\hspace*{0pt}strict{\char95}dequeue (AQueue xs []) =\\
+\hspace*{0pt} ~(if nulla xs then empty{\char95}queue else strict{\char95}dequeue (AQueue [] (rev xs)));%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
@@ -1290,7 +1289,7 @@
 %
 \begin{isamarkuptext}%
 \begin{isabelle}%
-lexord\ r\ {\isasymequiv}\isanewline
+lexord\ r\ {\isacharequal}\isanewline
 {\isacharbraceleft}{\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}{\isachardot}\isanewline
 \isaindent{\ }{\isasymexists}a\ v{\isachardot}\ y\ {\isacharequal}\ x\ {\isacharat}\ a\ {\isacharhash}\ v\ {\isasymor}\isanewline
 \isaindent{\ {\isasymexists}a\ v{\isachardot}\ }{\isacharparenleft}{\isasymexists}u\ a\ b\ v\ w{\isachardot}\ {\isacharparenleft}a{\isacharcomma}\ b{\isacharparenright}\ {\isasymin}\ r\ {\isasymand}\ x\ {\isacharequal}\ u\ {\isacharat}\ a\ {\isacharhash}\ v\ {\isasymand}\ y\ {\isacharequal}\ u\ {\isacharat}\ b\ {\isacharhash}\ w{\isacharparenright}{\isacharbraceright}%