updated
authorhaftmann
Fri Apr 20 13:11:47 2007 +0200 (2007-04-20)
changeset 227511bfd75c1f232
parent 22750 bff5d59de79b
child 22752 8b3131eeb509
updated
doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy
doc-src/IsarAdvanced/Codegen/Thy/document/Codegen.tex
doc-src/IsarAdvanced/Codegen/Thy/document/isabelle.sty
doc-src/IsarAdvanced/Codegen/Thy/examples/Codegen.hs
doc-src/IsarAdvanced/Codegen/Thy/examples/bool_literal.ML
doc-src/IsarAdvanced/Codegen/Thy/examples/class.ML
doc-src/IsarAdvanced/Codegen/Thy/examples/class.ocaml
doc-src/IsarAdvanced/Codegen/Thy/examples/collect_duplicates.ML
doc-src/IsarAdvanced/Codegen/Thy/examples/fac.ML
doc-src/IsarAdvanced/Codegen/Thy/examples/fac_case.ML
doc-src/IsarAdvanced/Codegen/Thy/examples/pick1.ML
doc-src/IsarAdvanced/Codegen/Thy/examples/pick2.ML
     1.1 --- a/doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy	Fri Apr 20 11:21:53 2007 +0200
     1.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy	Fri Apr 20 13:11:47 2007 +0200
     1.3 @@ -280,14 +280,11 @@
     1.4  text {*
     1.5    \noindent which displays a table of constant with corresponding
     1.6    defining equations (the additional stuff displayed
     1.7 -  shall not bother us for the moment). If this table does
     1.8 -  not provide at least one defining
     1.9 -  equation for a particular constant, the table of primitive
    1.10 -  definitions is searched
    1.11 -  whether it provides one.
    1.12 +  shall not bother us for the moment).
    1.13  
    1.14    The typical HOL tools are already set up in a way that
    1.15 -  function definitions introduced by @{text "\<FUN>"},
    1.16 +  function definitions introduced by @{text "\<DEFINITION>"},
    1.17 +  @{text "\<FUN>"},
    1.18    @{text "\<FUNCTION>"}, @{text "\<PRIMREC>"}
    1.19    @{text "\<RECDEF>"} are implicitly propagated
    1.20    to this defining equation table. Specific theorems may be
    1.21 @@ -861,15 +858,17 @@
    1.22  *}
    1.23  
    1.24  instance * :: (ord, ord) ord
    1.25 -  "p1 < p2 \<equiv> let (x1 \<Colon> 'a\<Colon>ord, y1 \<Colon> 'b\<Colon>ord) = p1; (x2, y2) = p2 in
    1.26 +  less_prod_def: "p1 < p2 \<equiv> let (x1 \<Colon> 'a\<Colon>ord, y1 \<Colon> 'b\<Colon>ord) = p1; (x2, y2) = p2 in
    1.27      x1 < x2 \<or> (x1 = x2 \<and> y1 < y2)"
    1.28 -  "p1 \<le> p2 \<equiv> let (x1 \<Colon> 'a\<Colon>ord, y1 \<Colon> 'b\<Colon>ord) = p1; (x2, y2) = p2 in
    1.29 +  less_eq_prod_def: "p1 \<le> p2 \<equiv> let (x1 \<Colon> 'a\<Colon>ord, y1 \<Colon> 'b\<Colon>ord) = p1; (x2, y2) = p2 in
    1.30      x1 < x2 \<or> (x1 = x2 \<and> y1 \<le> y2)" ..
    1.31  
    1.32 +lemmas [code nofunc] = less_prod_def less_eq_prod_def
    1.33 +
    1.34  lemma ord_prod [code func]:
    1.35    "(x1 \<Colon> 'a\<Colon>ord, y1 \<Colon> 'b\<Colon>ord) < (x2, y2) \<longleftrightarrow> x1 < x2 \<or> (x1 = x2 \<and> y1 < y2)"
    1.36    "(x1 \<Colon> 'a\<Colon>ord, y1 \<Colon> 'b\<Colon>ord) \<le> (x2, y2) \<longleftrightarrow> x1 < x2 \<or> (x1 = x2 \<and> y1 \<le> y2)"
    1.37 -  unfolding "less_eq_*_def" "less_*_def" by simp_all
    1.38 +  unfolding less_prod_def less_eq_prod_def by simp_all
    1.39  
    1.40  text {*
    1.41    Then code generation will fail.  Why?  The definition
    1.42 @@ -883,7 +882,7 @@
    1.43  *}
    1.44  
    1.45  (*<*)
    1.46 -declare ord_prod [code del]
    1.47 +lemmas [code nofunc] = ord_prod
    1.48  (*>*)
    1.49  
    1.50  lemma ord_prod_code [code func]:
    1.51 @@ -907,7 +906,10 @@
    1.52    restrictive sort constraints than the underlying instance relation
    1.53    between class and type constructor as long as the whole system of
    1.54    constraints is coregular; code theorems violating coregularity
    1.55 -  are rejected immediately.
    1.56 +  are rejected immediately.  Consequently, it might be necessary
    1.57 +  to delete disturbing theorems in the code theorem table,
    1.58 +  as we have done here with the original definitions @{text less_prod_def}
    1.59 +  and @{text less_eq_prod_def}.
    1.60  *}
    1.61  
    1.62  subsubsection {* Haskell serialization *}
    1.63 @@ -1002,7 +1004,7 @@
    1.64    expects dictionaries (namely an \emph{eq} dictionary) but
    1.65    has also been given a customary serialization.
    1.66  
    1.67 -  The solution to this dilemma:
    1.68 +  \fixme[needs rewrite] The solution to this dilemma:
    1.69  *}
    1.70  
    1.71  lemma [code func]:
    1.72 @@ -1013,9 +1015,7 @@
    1.73  text {*
    1.74    \lstsml{Thy/examples/dirty_set.ML}
    1.75  
    1.76 -  Reflexive defining equations by convention are dropped.
    1.77 -  But their presence prevents primitive definitions to be
    1.78 -  used as defining equations:
    1.79 +  Reflexive defining equations by convention are dropped:
    1.80  *}
    1.81  
    1.82  code_thms insert
    1.83 @@ -1201,12 +1201,12 @@
    1.84  
    1.85  text %mlref {*
    1.86    \begin{mldecls}
    1.87 -  @{index_ML CodegenData.lazy: "(unit -> thm list) -> thm list Susp.T"}
    1.88 +  @{index_ML CodegenData.lazy_thms: "(unit -> thm list) -> thm list Susp.T"}
    1.89    \end{mldecls}
    1.90  
    1.91    \begin{description}
    1.92  
    1.93 -  \item @{ML CodegenData.lazy}~@{text f} turns an abstract
    1.94 +  \item @{ML CodegenData.lazy_thms}~@{text f} turns an abstract
    1.95       theorem computation @{text f} into a suspension of theorems.
    1.96  
    1.97    \end{description}
    1.98 @@ -1294,7 +1294,7 @@
    1.99    @{index_ML CodegenConsts.eq_const: "CodegenConsts.const * CodegenConsts.const -> bool"} \\
   1.100    @{index_ML CodegenConsts.read_const: "theory -> string -> CodegenConsts.const"} \\
   1.101    @{index_ML_structure CodegenConsts.Consttab} \\
   1.102 -  @{index_ML CodegenFunc.typ_func: "thm -> typ"} \\
   1.103 +  @{index_ML CodegenFunc.head_func: "thm -> CodegenConsts.const * typ"} \\
   1.104    @{index_ML CodegenFunc.rewrite_func: "thm list -> thm -> thm"} \\
   1.105    \end{mldecls}
   1.106  
   1.107 @@ -1309,8 +1309,8 @@
   1.108    \item @{ML CodegenConsts.read_const}~@{text thy}~@{text s}
   1.109       reads a constant as a concrete term expression @{text s}.
   1.110  
   1.111 -  \item @{ML CodegenFunc.typ_func}~@{text thm}
   1.112 -     extracts the type of a constant in a defining equation @{text thm}.
   1.113 +  \item @{ML CodegenFunc.head_func}~@{text thm}
   1.114 +     extracts the constant and its type from a defining equation @{text thm}.
   1.115  
   1.116    \item @{ML CodegenFunc.rewrite_func}~@{text rews}~@{text thm}
   1.117       rewrites a defining equation @{text thm} with a set of rewrite
     2.1 --- a/doc-src/IsarAdvanced/Codegen/Thy/document/Codegen.tex	Fri Apr 20 11:21:53 2007 +0200
     2.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/document/Codegen.tex	Fri Apr 20 13:11:47 2007 +0200
     2.3 @@ -332,14 +332,11 @@
     2.4  \begin{isamarkuptext}%
     2.5  \noindent which displays a table of constant with corresponding
     2.6    defining equations (the additional stuff displayed
     2.7 -  shall not bother us for the moment). If this table does
     2.8 -  not provide at least one defining
     2.9 -  equation for a particular constant, the table of primitive
    2.10 -  definitions is searched
    2.11 -  whether it provides one.
    2.12 +  shall not bother us for the moment).
    2.13  
    2.14    The typical HOL tools are already set up in a way that
    2.15 -  function definitions introduced by \isa{{\isasymFUN}},
    2.16 +  function definitions introduced by \isa{{\isasymDEFINITION}},
    2.17 +  \isa{{\isasymFUN}},
    2.18    \isa{{\isasymFUNCTION}}, \isa{{\isasymPRIMREC}}
    2.19    \isa{{\isasymRECDEF}} are implicitly propagated
    2.20    to this defining equation table. Specific theorems may be
    2.21 @@ -1154,9 +1151,9 @@
    2.22  \isamarkuptrue%
    2.23  \isacommand{instance}\isamarkupfalse%
    2.24  \ {\isacharasterisk}\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}ord{\isacharcomma}\ ord{\isacharparenright}\ ord\isanewline
    2.25 -\ \ {\isachardoublequoteopen}p{\isadigit{1}}\ {\isacharless}\ p{\isadigit{2}}\ {\isasymequiv}\ let\ {\isacharparenleft}x{\isadigit{1}}\ {\isasymColon}\ {\isacharprime}a{\isasymColon}ord{\isacharcomma}\ y{\isadigit{1}}\ {\isasymColon}\ {\isacharprime}b{\isasymColon}ord{\isacharparenright}\ {\isacharequal}\ p{\isadigit{1}}{\isacharsemicolon}\ {\isacharparenleft}x{\isadigit{2}}{\isacharcomma}\ y{\isadigit{2}}{\isacharparenright}\ {\isacharequal}\ p{\isadigit{2}}\ in\isanewline
    2.26 +\ \ less{\isacharunderscore}prod{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}p{\isadigit{1}}\ {\isacharless}\ p{\isadigit{2}}\ {\isasymequiv}\ let\ {\isacharparenleft}x{\isadigit{1}}\ {\isasymColon}\ {\isacharprime}a{\isasymColon}ord{\isacharcomma}\ y{\isadigit{1}}\ {\isasymColon}\ {\isacharprime}b{\isasymColon}ord{\isacharparenright}\ {\isacharequal}\ p{\isadigit{1}}{\isacharsemicolon}\ {\isacharparenleft}x{\isadigit{2}}{\isacharcomma}\ y{\isadigit{2}}{\isacharparenright}\ {\isacharequal}\ p{\isadigit{2}}\ in\isanewline
    2.27  \ \ \ \ x{\isadigit{1}}\ {\isacharless}\ x{\isadigit{2}}\ {\isasymor}\ {\isacharparenleft}x{\isadigit{1}}\ {\isacharequal}\ x{\isadigit{2}}\ {\isasymand}\ y{\isadigit{1}}\ {\isacharless}\ y{\isadigit{2}}{\isacharparenright}{\isachardoublequoteclose}\isanewline
    2.28 -\ \ {\isachardoublequoteopen}p{\isadigit{1}}\ {\isasymle}\ p{\isadigit{2}}\ {\isasymequiv}\ let\ {\isacharparenleft}x{\isadigit{1}}\ {\isasymColon}\ {\isacharprime}a{\isasymColon}ord{\isacharcomma}\ y{\isadigit{1}}\ {\isasymColon}\ {\isacharprime}b{\isasymColon}ord{\isacharparenright}\ {\isacharequal}\ p{\isadigit{1}}{\isacharsemicolon}\ {\isacharparenleft}x{\isadigit{2}}{\isacharcomma}\ y{\isadigit{2}}{\isacharparenright}\ {\isacharequal}\ p{\isadigit{2}}\ in\isanewline
    2.29 +\ \ less{\isacharunderscore}eq{\isacharunderscore}prod{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}p{\isadigit{1}}\ {\isasymle}\ p{\isadigit{2}}\ {\isasymequiv}\ let\ {\isacharparenleft}x{\isadigit{1}}\ {\isasymColon}\ {\isacharprime}a{\isasymColon}ord{\isacharcomma}\ y{\isadigit{1}}\ {\isasymColon}\ {\isacharprime}b{\isasymColon}ord{\isacharparenright}\ {\isacharequal}\ p{\isadigit{1}}{\isacharsemicolon}\ {\isacharparenleft}x{\isadigit{2}}{\isacharcomma}\ y{\isadigit{2}}{\isacharparenright}\ {\isacharequal}\ p{\isadigit{2}}\ in\isanewline
    2.30  \ \ \ \ x{\isadigit{1}}\ {\isacharless}\ x{\isadigit{2}}\ {\isasymor}\ {\isacharparenleft}x{\isadigit{1}}\ {\isacharequal}\ x{\isadigit{2}}\ {\isasymand}\ y{\isadigit{1}}\ {\isasymle}\ y{\isadigit{2}}{\isacharparenright}{\isachardoublequoteclose}%
    2.31  \isadelimproof
    2.32  \ %
    2.33 @@ -1173,6 +1170,9 @@
    2.34  \endisadelimproof
    2.35  \isanewline
    2.36  \isanewline
    2.37 +\isacommand{lemmas}\isamarkupfalse%
    2.38 +\ {\isacharbrackleft}code\ nofunc{\isacharbrackright}\ {\isacharequal}\ less{\isacharunderscore}prod{\isacharunderscore}def\ less{\isacharunderscore}eq{\isacharunderscore}prod{\isacharunderscore}def\isanewline
    2.39 +\isanewline
    2.40  \isacommand{lemma}\isamarkupfalse%
    2.41  \ ord{\isacharunderscore}prod\ {\isacharbrackleft}code\ func{\isacharbrackright}{\isacharcolon}\isanewline
    2.42  \ \ {\isachardoublequoteopen}{\isacharparenleft}x{\isadigit{1}}\ {\isasymColon}\ {\isacharprime}a{\isasymColon}ord{\isacharcomma}\ y{\isadigit{1}}\ {\isasymColon}\ {\isacharprime}b{\isasymColon}ord{\isacharparenright}\ {\isacharless}\ {\isacharparenleft}x{\isadigit{2}}{\isacharcomma}\ y{\isadigit{2}}{\isacharparenright}\ {\isasymlongleftrightarrow}\ x{\isadigit{1}}\ {\isacharless}\ x{\isadigit{2}}\ {\isasymor}\ {\isacharparenleft}x{\isadigit{1}}\ {\isacharequal}\ x{\isadigit{2}}\ {\isasymand}\ y{\isadigit{1}}\ {\isacharless}\ y{\isadigit{2}}{\isacharparenright}{\isachardoublequoteclose}\isanewline
    2.43 @@ -1184,7 +1184,7 @@
    2.44  %
    2.45  \isatagproof
    2.46  \isacommand{unfolding}\isamarkupfalse%
    2.47 -\ {\isachardoublequoteopen}less{\isacharunderscore}eq{\isacharunderscore}{\isacharasterisk}{\isacharunderscore}def{\isachardoublequoteclose}\ {\isachardoublequoteopen}less{\isacharunderscore}{\isacharasterisk}{\isacharunderscore}def{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
    2.48 +\ less{\isacharunderscore}prod{\isacharunderscore}def\ less{\isacharunderscore}eq{\isacharunderscore}prod{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse%
    2.49  \ simp{\isacharunderscore}all%
    2.50  \endisatagproof
    2.51  {\isafoldproof}%
    2.52 @@ -1242,7 +1242,10 @@
    2.53    restrictive sort constraints than the underlying instance relation
    2.54    between class and type constructor as long as the whole system of
    2.55    constraints is coregular; code theorems violating coregularity
    2.56 -  are rejected immediately.%
    2.57 +  are rejected immediately.  Consequently, it might be necessary
    2.58 +  to delete disturbing theorems in the code theorem table,
    2.59 +  as we have done here with the original definitions \isa{less{\isacharunderscore}prod{\isacharunderscore}def}
    2.60 +  and \isa{less{\isacharunderscore}eq{\isacharunderscore}prod{\isacharunderscore}def}.%
    2.61  \end{isamarkuptext}%
    2.62  \isamarkuptrue%
    2.63  %
    2.64 @@ -1430,7 +1433,7 @@
    2.65    expects dictionaries (namely an \emph{eq} dictionary) but
    2.66    has also been given a customary serialization.
    2.67  
    2.68 -  The solution to this dilemma:%
    2.69 +  \fixme[needs rewrite] The solution to this dilemma:%
    2.70  \end{isamarkuptext}%
    2.71  \isamarkuptrue%
    2.72  \isacommand{lemma}\isamarkupfalse%
    2.73 @@ -1456,9 +1459,7 @@
    2.74  \begin{isamarkuptext}%
    2.75  \lstsml{Thy/examples/dirty_set.ML}
    2.76  
    2.77 -  Reflexive defining equations by convention are dropped.
    2.78 -  But their presence prevents primitive definitions to be
    2.79 -  used as defining equations:%
    2.80 +  Reflexive defining equations by convention are dropped:%
    2.81  \end{isamarkuptext}%
    2.82  \isamarkuptrue%
    2.83  \isacommand{code{\isacharunderscore}thms}\isamarkupfalse%
    2.84 @@ -1697,12 +1698,12 @@
    2.85  %
    2.86  \begin{isamarkuptext}%
    2.87  \begin{mldecls}
    2.88 -  \indexml{CodegenData.lazy}\verb|CodegenData.lazy: (unit -> thm list) -> thm list Susp.T|
    2.89 +  \indexml{CodegenData.lazy-thms}\verb|CodegenData.lazy_thms: (unit -> thm list) -> thm list Susp.T|
    2.90    \end{mldecls}
    2.91  
    2.92    \begin{description}
    2.93  
    2.94 -  \item \verb|CodegenData.lazy|~\isa{f} turns an abstract
    2.95 +  \item \verb|CodegenData.lazy_thms|~\isa{f} turns an abstract
    2.96       theorem computation \isa{f} into a suspension of theorems.
    2.97  
    2.98    \end{description}%
    2.99 @@ -1822,7 +1823,7 @@
   2.100    \indexml{CodegenConsts.eq-const}\verb|CodegenConsts.eq_const: CodegenConsts.const * CodegenConsts.const -> bool| \\
   2.101    \indexml{CodegenConsts.read-const}\verb|CodegenConsts.read_const: theory -> string -> CodegenConsts.const| \\
   2.102    \indexmlstructure{CodegenConsts.Consttab}\verb|structure CodegenConsts.Consttab| \\
   2.103 -  \indexml{CodegenFunc.typ-func}\verb|CodegenFunc.typ_func: thm -> typ| \\
   2.104 +  \indexml{CodegenFunc.head-func}\verb|CodegenFunc.head_func: thm -> CodegenConsts.const * typ| \\
   2.105    \indexml{CodegenFunc.rewrite-func}\verb|CodegenFunc.rewrite_func: thm list -> thm -> thm| \\
   2.106    \end{mldecls}
   2.107  
   2.108 @@ -1837,8 +1838,8 @@
   2.109    \item \verb|CodegenConsts.read_const|~\isa{thy}~\isa{s}
   2.110       reads a constant as a concrete term expression \isa{s}.
   2.111  
   2.112 -  \item \verb|CodegenFunc.typ_func|~\isa{thm}
   2.113 -     extracts the type of a constant in a defining equation \isa{thm}.
   2.114 +  \item \verb|CodegenFunc.head_func|~\isa{thm}
   2.115 +     extracts the constant and its type from a defining equation \isa{thm}.
   2.116  
   2.117    \item \verb|CodegenFunc.rewrite_func|~\isa{rews}~\isa{thm}
   2.118       rewrites a defining equation \isa{thm} with a set of rewrite
     3.1 --- a/doc-src/IsarAdvanced/Codegen/Thy/document/isabelle.sty	Fri Apr 20 11:21:53 2007 +0200
     3.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/document/isabelle.sty	Fri Apr 20 13:11:47 2007 +0200
     3.3 @@ -31,6 +31,7 @@
     3.4  \newcommand{\isactrlesup}{\egroup\egroup\end{math}\egroup}
     3.5  \newcommand{\isactrlbold}[1]{{\bfseries\upshape\boldmath#1}}
     3.6  \newcommand{\isactrlloc}[1]{{\bfseries\upshape\boldmath#1}}
     3.7 +\newenvironment{isaantiq}{{\isacharat\isacharbraceleft}}{{\isacharbraceright}}
     3.8  
     3.9  
    3.10  \newdimen\isa@parindent\newdimen\isa@parskip
     4.1 --- a/doc-src/IsarAdvanced/Codegen/Thy/examples/Codegen.hs	Fri Apr 20 11:21:53 2007 +0200
     4.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/Codegen.hs	Fri Apr 20 13:11:47 2007 +0200
     4.3 @@ -7,7 +7,7 @@
     4.4  };
     4.5  
     4.6  heada :: (Codegen.Null a) => [a] -> a;
     4.7 -heada (y : xs) = y;
     4.8 +heada (x : xs) = x;
     4.9  heada [] = Codegen.nulla;
    4.10  
    4.11  null_option :: Maybe a;
     5.1 --- a/doc-src/IsarAdvanced/Codegen/Thy/examples/bool_literal.ML	Fri Apr 20 11:21:53 2007 +0200
     5.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/bool_literal.ML	Fri Apr 20 13:11:47 2007 +0200
     5.3 @@ -6,9 +6,9 @@
     5.4  
     5.5  datatype boola = True | False;
     5.6  
     5.7 -fun op_and y True = y
     5.8 +fun op_and x True = x
     5.9    | op_and x False = False
    5.10 -  | op_and True y = y
    5.11 +  | op_and True x = x
    5.12    | op_and False x = False;
    5.13  
    5.14  end; (*struct HOL*)
     6.1 --- a/doc-src/IsarAdvanced/Codegen/Thy/examples/class.ML	Fri Apr 20 11:21:53 2007 +0200
     6.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/class.ML	Fri Apr 20 13:11:47 2007 +0200
     6.3 @@ -14,7 +14,7 @@
     6.4  type 'a null = {null : 'a};
     6.5  fun null (A_:'a null) = #null A_;
     6.6  
     6.7 -fun head A_ (y :: xs) = y
     6.8 +fun head A_ (x :: xs) = x
     6.9    | head A_ [] = null A_;
    6.10  
    6.11  val null_option : 'a option = NONE;
     7.1 --- a/doc-src/IsarAdvanced/Codegen/Thy/examples/class.ocaml	Fri Apr 20 11:21:53 2007 +0200
     7.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/class.ocaml	Fri Apr 20 13:11:47 2007 +0200
     7.3 @@ -14,7 +14,7 @@
     7.4  type 'a null = {null : 'a};;
     7.5  let null _A = _A.null;;
     7.6  
     7.7 -let rec head _A = function y :: xs -> y
     7.8 +let rec head _A = function x :: xs -> x
     7.9                    | [] -> null _A;;
    7.10  
    7.11  let rec null_option = None;;
     8.1 --- a/doc-src/IsarAdvanced/Codegen/Thy/examples/collect_duplicates.ML	Fri Apr 20 11:21:53 2007 +0200
     8.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/collect_duplicates.ML	Fri Apr 20 13:11:47 2007 +0200
     8.3 @@ -26,7 +26,7 @@
     8.4      then (if List.memberl A_ z ys then collect_duplicates A_ xs ys zs
     8.5             else collect_duplicates A_ xs (z :: ys) zs)
     8.6      else collect_duplicates A_ (z :: xs) (z :: ys) zs)
     8.7 -  | collect_duplicates A_ y ys [] = y;
     8.8 +  | collect_duplicates A_ xs ys [] = xs;
     8.9  
    8.10  end; (*struct Codegen*)
    8.11  
     9.1 --- a/doc-src/IsarAdvanced/Codegen/Thy/examples/fac.ML	Fri Apr 20 11:21:53 2007 +0200
     9.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/fac.ML	Fri Apr 20 13:11:47 2007 +0200
     9.3 @@ -7,7 +7,7 @@
     9.4  datatype nat = Zero_nat | Suc of nat;
     9.5  
     9.6  fun plus_nat (Suc m) n = plus_nat m (Suc n)
     9.7 -  | plus_nat Zero_nat y = y;
     9.8 +  | plus_nat Zero_nat n = n;
     9.9  
    9.10  fun times_nat (Suc m) n = plus_nat n (times_nat m n)
    9.11    | times_nat Zero_nat n = Zero_nat;
    10.1 --- a/doc-src/IsarAdvanced/Codegen/Thy/examples/fac_case.ML	Fri Apr 20 11:21:53 2007 +0200
    10.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/fac_case.ML	Fri Apr 20 13:11:47 2007 +0200
    10.3 @@ -7,7 +7,7 @@
    10.4  datatype nat = Zero_nat | Suc of nat;
    10.5  
    10.6  fun plus_nat (Suc m) n = plus_nat m (Suc n)
    10.7 -  | plus_nat Zero_nat y = y;
    10.8 +  | plus_nat Zero_nat n = n;
    10.9  
   10.10  fun times_nat (Suc m) n = plus_nat n (times_nat m n)
   10.11    | times_nat Zero_nat n = Zero_nat;
    11.1 --- a/doc-src/IsarAdvanced/Codegen/Thy/examples/pick1.ML	Fri Apr 20 11:21:53 2007 +0200
    11.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/pick1.ML	Fri Apr 20 13:11:47 2007 +0200
    11.3 @@ -13,7 +13,7 @@
    11.4  
    11.5  fun minus_nat (Suc m) (Suc n) = minus_nat m n
    11.6    | minus_nat Zero_nat n = Zero_nat
    11.7 -  | minus_nat y Zero_nat = y;
    11.8 +  | minus_nat m Zero_nat = m;
    11.9  
   11.10  end; (*struct Nat*)
   11.11  
    12.1 --- a/doc-src/IsarAdvanced/Codegen/Thy/examples/pick2.ML	Fri Apr 20 11:21:53 2007 +0200
    12.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/pick2.ML	Fri Apr 20 13:11:47 2007 +0200
    12.3 @@ -13,7 +13,7 @@
    12.4  
    12.5  fun minus_nat (Suc m) (Suc n) = minus_nat m n
    12.6    | minus_nat Zero_nat n = Zero_nat
    12.7 -  | minus_nat y Zero_nat = y;
    12.8 +  | minus_nat m Zero_nat = m;
    12.9  
   12.10  end; (*struct Nat*)
   12.11