1.1 --- a/doc-src/Codegen/Thy/document/ML.tex	Mon May 31 17:29:28 2010 +0200
     1.2 +++ b/doc-src/Codegen/Thy/document/ML.tex	Mon May 31 17:31:33 2010 +0200
     1.3 @@ -60,9 +60,9 @@
     1.4  \verb|    -> theory -> theory| \\
     1.5    \indexdef{}{ML}{Code\_Preproc.del\_functrans}\verb|Code_Preproc.del_functrans: string -> theory -> theory| \\
     1.6    \indexdef{}{ML}{Code.add\_datatype}\verb|Code.add_datatype: (string * typ) list -> theory -> theory| \\
     1.7 -  \indexdef{}{ML}{Code.get\_datatype}\verb|Code.get_datatype: theory -> string|\isasep\isanewline%
     1.8 +  \indexdef{}{ML}{Code.get\_type}\verb|Code.get_type: theory -> string|\isasep\isanewline%
     1.9  \verb|    -> (string * sort) list * (string * typ list) list| \\
    1.10 -  \indexdef{}{ML}{Code.get\_datatype\_of\_constr}\verb|Code.get_datatype_of_constr: theory -> string -> string option|
    1.11 +  \indexdef{}{ML}{Code.get\_type\_of\_constr\_or\_abstr}\verb|Code.get_type_of_constr_or_abstr: theory -> string -> (string * bool) option|
    1.12    \end{mldecls}
    1.13  
    1.14    \begin{description}
    1.15 @@ -91,7 +91,7 @@
    1.16       a datatype to executable content, with generation
    1.17       set \isa{cs}.
    1.18  
    1.19 -  \item \verb|Code.get_datatype_of_constr|~\isa{thy}~\isa{const}
    1.20 +  \item \verb|Code.get_type_of_constr_or_abstr|~\isa{thy}~\isa{const}
    1.21       returns type constructor corresponding to
    1.22       constructor \isa{const}; returns \isa{NONE}
    1.23       if \isa{const} is no constructor.
    1.24 @@ -163,7 +163,7 @@
    1.25    merge, which is a little bit nasty from an implementation
    1.26    point of view.  The framework provides a solution
    1.27    to this technical challenge by providing a functorial
    1.28 -  data slot \verb|CodeDataFun|; on instantiation
    1.29 +  data slot \verb|Code_Data|; on instantiation
    1.30    of this functor, the following types and operations
    1.31    are required:
    1.32  
    1.33 @@ -189,7 +189,7 @@
    1.34  
    1.35    \end{description}
    1.36  
    1.37 -  \noindent An instance of \verb|CodeDataFun| provides the following
    1.38 +  \noindent An instance of \verb|Code_Data| provides the following
    1.39    interface:
    1.40  
    1.41    \medskip

     2.1 --- a/doc-src/Codegen/Thy/document/Program.tex	Mon May 31 17:29:28 2010 +0200
     2.2 +++ b/doc-src/Codegen/Thy/document/Program.tex	Mon May 31 17:31:33 2010 +0200
     2.3 @@ -432,9 +432,9 @@
     2.4  %
     2.5  \isatagquote
     2.6  \isacommand{lemma}\isamarkupfalse%
     2.7 -\ {\isacharbrackleft}code{\isacharunderscore}inline{\isacharbrackright}{\isacharcolon}\isanewline
     2.8 -\ \ {\isachardoublequoteopen}x\ {\isasymin}\ set\ xs\ {\isasymlongleftrightarrow}\ x\ mem\ xs{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
     2.9 -\ {\isacharparenleft}induct\ xs{\isacharparenright}\ simp{\isacharunderscore}all%
    2.10 +\ {\isacharbrackleft}code{\isacharunderscore}unfold{\isacharbrackright}{\isacharcolon}\isanewline
    2.11 +\ \ {\isachardoublequoteopen}x\ {\isasymin}\ set\ xs\ {\isasymlongleftrightarrow}\ member\ xs\ x{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
    2.12 +\ {\isacharparenleft}fact\ in{\isacharunderscore}set{\isacharunderscore}code{\isacharparenright}%
    2.13  \endisatagquote
    2.14  {\isafoldquote}%
    2.15  %
    2.16 @@ -453,9 +453,9 @@
    2.17  %
    2.18  \isatagquote
    2.19  \isacommand{lemma}\isamarkupfalse%
    2.20 -\ {\isacharbrackleft}code{\isacharunderscore}inline{\isacharbrackright}{\isacharcolon}\isanewline
    2.21 +\ {\isacharbrackleft}code{\isacharunderscore}unfold{\isacharbrackright}{\isacharcolon}\isanewline
    2.22  \ \ {\isachardoublequoteopen}{\isadigit{1}}\ {\isacharequal}\ Suc\ {\isadigit{0}}{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
    2.23 -\ simp%
    2.24 +\ {\isacharparenleft}fact\ One{\isacharunderscore}nat{\isacharunderscore}def{\isacharparenright}%
    2.25  \endisatagquote
    2.26  {\isafoldquote}%
    2.27  %
    2.28 @@ -474,9 +474,9 @@
    2.29  %
    2.30  \isatagquote
    2.31  \isacommand{lemma}\isamarkupfalse%
    2.32 -\ {\isacharbrackleft}code{\isacharunderscore}inline{\isacharbrackright}{\isacharcolon}\isanewline
    2.33 +\ {\isacharbrackleft}code{\isacharunderscore}unfold{\isacharbrackright}{\isacharcolon}\isanewline
    2.34  \ \ {\isachardoublequoteopen}xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymlongleftrightarrow}\ List{\isachardot}null\ xs{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
    2.35 -\ {\isacharparenleft}induct\ xs{\isacharparenright}\ simp{\isacharunderscore}all%
    2.36 +\ {\isacharparenleft}fact\ empty{\isacharunderscore}null{\isacharparenright}%
    2.37  \endisatagquote
    2.38  {\isafoldquote}%
    2.39  %
    2.40 @@ -763,7 +763,7 @@
    2.41  %
    2.42  \begin{isamarkuptext}%
    2.43  \noindent The membership test during preprocessing is rewritten,
    2.44 -  resulting in \isa{op\ mem}, which itself
    2.45 +  resulting in \isa{member}, which itself
    2.46    performs an explicit equality check.%
    2.47  \end{isamarkuptext}%
    2.48  \isamarkuptrue%
    2.49 @@ -781,7 +781,7 @@
    2.50  \hspace*{0pt} ~type 'a eq\\
    2.51  \hspace*{0pt} ~val eq :~'a eq -> 'a -> 'a -> bool\\
    2.52  \hspace*{0pt} ~val eqa :~'a eq -> 'a -> 'a -> bool\\
    2.53 -\hspace*{0pt} ~val member :~'a eq -> 'a -> 'a list -> bool\\
    2.54 +\hspace*{0pt} ~val member :~'a eq -> 'a list -> 'a -> bool\\
    2.55  \hspace*{0pt} ~val collect{\char95}duplicates :\\
    2.56  \hspace*{0pt} ~~~'a eq -> 'a list -> 'a list -> 'a list -> 'a list\\
    2.57  \hspace*{0pt}end = struct\\
    2.58 @@ -791,13 +791,13 @@
    2.59  \hspace*{0pt}\\
    2.60  \hspace*{0pt}fun eqa A{\char95}~a b = eq A{\char95}~a b;\\
    2.61  \hspace*{0pt}\\
    2.62 -\hspace*{0pt}fun member A{\char95}~x [] = false\\
    2.63 -\hspace*{0pt} ~| member A{\char95}~x (y ::~ys) = eqa A{\char95}~x y orelse member A{\char95}~x ys;\\
    2.64 +\hspace*{0pt}fun member A{\char95}~[] y = false\\
    2.65 +\hspace*{0pt} ~| member A{\char95}~(x ::~xs) y = eqa A{\char95}~x y orelse member A{\char95}~xs y;\\
    2.66  \hspace*{0pt}\\
    2.67  \hspace*{0pt}fun collect{\char95}duplicates A{\char95}~xs ys [] = xs\\
    2.68  \hspace*{0pt} ~| collect{\char95}duplicates A{\char95}~xs ys (z ::~zs) =\\
    2.69 -\hspace*{0pt} ~~~(if member A{\char95}~z xs\\
    2.70 -\hspace*{0pt} ~~~~~then (if member A{\char95}~z ys then collect{\char95}duplicates A{\char95}~xs ys zs\\
    2.71 +\hspace*{0pt} ~~~(if member A{\char95}~xs z\\
    2.72 +\hspace*{0pt} ~~~~~then (if member A{\char95}~ys z then collect{\char95}duplicates A{\char95}~xs ys zs\\
    2.73  \hspace*{0pt} ~~~~~~~~~~~~else collect{\char95}duplicates A{\char95}~xs (z ::~ys) zs)\\
    2.74  \hspace*{0pt} ~~~~~else collect{\char95}duplicates A{\char95}~(z ::~xs) (z ::~ys) zs);\\
    2.75  \hspace*{0pt}\\
    2.76 @@ -968,11 +968,10 @@
    2.77  \hspace*{0pt}empty{\char95}queue ::~forall a.~a;\\
    2.78  \hspace*{0pt}empty{\char95}queue = error {\char34}empty{\char95}queue{\char34};\\
    2.79  \hspace*{0pt}\\
    2.80 -\hspace*{0pt}strict{\char95}dequeue' ::~forall a.~Queue a -> (a,~Queue a);\\
    2.81 -\hspace*{0pt}strict{\char95}dequeue' (AQueue xs (y :~ys)) = (y,~AQueue xs ys);\\
    2.82 -\hspace*{0pt}strict{\char95}dequeue' (AQueue xs []) =\\
    2.83 -\hspace*{0pt} ~(if nulla xs then empty{\char95}queue\\
    2.84 -\hspace*{0pt} ~~~else strict{\char95}dequeue' (AQueue [] (rev xs)));%
    2.85 +\hspace*{0pt}strict{\char95}dequeue ::~forall a.~Queue a -> (a,~Queue a);\\
    2.86 +\hspace*{0pt}strict{\char95}dequeue (AQueue xs (y :~ys)) = (y,~AQueue xs ys);\\
    2.87 +\hspace*{0pt}strict{\char95}dequeue (AQueue xs []) =\\
    2.88 +\hspace*{0pt} ~(if nulla xs then empty{\char95}queue else strict{\char95}dequeue (AQueue [] (rev xs)));%
    2.89  \end{isamarkuptext}%
    2.90  \isamarkuptrue%
    2.91  %
    2.92 @@ -1290,7 +1289,7 @@
    2.93  %
    2.94  \begin{isamarkuptext}%
    2.95  \begin{isabelle}%
    2.96 -lexord\ r\ {\isasymequiv}\isanewline
    2.97 +lexord\ r\ {\isacharequal}\isanewline
    2.98  {\isacharbraceleft}{\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}{\isachardot}\isanewline
    2.99  \isaindent{\ }{\isasymexists}a\ v{\isachardot}\ y\ {\isacharequal}\ x\ {\isacharat}\ a\ {\isacharhash}\ v\ {\isasymor}\isanewline
   2.100  \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}%