updated
authorhaftmann
Fri Aug 24 14:14:17 2007 +0200 (2007-08-24)
changeset 24421acfb2413faa3
parent 24420 9fa337721689
child 24422 c0b5ff9e9e4d
updated
doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy
doc-src/IsarAdvanced/Codegen/Thy/document/Codegen.tex
doc-src/IsarAdvanced/Codegen/Thy/examples/Codegen.hs
doc-src/IsarAdvanced/Codegen/Thy/examples/bool_infix.ML
doc-src/IsarAdvanced/Codegen/Thy/examples/bool_literal.ML
doc-src/IsarAdvanced/Codegen/Thy/examples/bool_mlbool.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/lexicographic.ML
doc-src/IsarAdvanced/Codegen/Thy/examples/monotype.ML
doc-src/IsarAdvanced/Codegen/Thy/examples/pick1.ML
doc-src/IsarAdvanced/Codegen/Thy/examples/pick2.ML
doc-src/IsarAdvanced/Codegen/Thy/examples/set_list.ML
doc-src/IsarAdvanced/Codegen/Thy/examples/tree.ML
     1.1 --- a/doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy	Fri Aug 24 14:14:16 2007 +0200
     1.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy	Fri Aug 24 14:14:17 2007 +0200
     1.3 @@ -469,8 +469,6 @@
     1.4      \item[@{text "Pretty_Char_chr"}] like @{text "Pretty_Char"},
     1.5         but also offers treatment of character codes; includes
     1.6         @{text "Pretty_Int"}.
     1.7 -    \item[@{text "Executable_Set"}] allows to generate code
     1.8 -       for finite sets using lists.
     1.9      \item[@{text "Executable_Rat"}] implements rational
    1.10         numbers.
    1.11      \item[@{text "Executable_Real"}] implements a subset of real numbers,
    1.12 @@ -935,7 +933,7 @@
    1.13    how to implement finite sets by lists
    1.14    using the conversion @{term [source] "set \<Colon> 'a list \<Rightarrow> 'a set"}
    1.15    as constructor:
    1.16 -*}
    1.17 +*} (*<*)ML {* nonfix union *} lemmas [code func del] = in_code union_empty1 union_empty2 union_insert Union_code(*>*)
    1.18  
    1.19  code_datatype set
    1.20  
    1.21 @@ -1018,35 +1016,6 @@
    1.22    description of the most important ML interfaces.
    1.23  *}
    1.24  
    1.25 -subsection {* Basics: @{text CodeUnit} *}
    1.26 -
    1.27 -text {*
    1.28 -  This module provides identification of (probably overloaded)
    1.29 -  constants by unique identifiers.
    1.30 -*}
    1.31 -
    1.32 -text %mlref {*
    1.33 -  \begin{mldecls}
    1.34 -  @{index_ML_type CodeUnit.const: "string * string option"} \\
    1.35 -  @{index_ML CodeUnit.const_of_cexpr: "theory -> string * typ -> CodeUnit.const"} \\
    1.36 - \end{mldecls}
    1.37 -
    1.38 -  \begin{description}
    1.39 -
    1.40 -  \item @{ML_type CodeUnit.const} is the identifier type:
    1.41 -     the product of a \emph{string} with a list of \emph{typs}.
    1.42 -     The \emph{string} is the constant name as represented inside Isabelle;
    1.43 -     for overloaded constants, the attached \emph{string option}
    1.44 -     is either @{text SOME} type constructor denoting an instance,
    1.45 -     or @{text NONE} for the polymorphic constant.
    1.46 -
    1.47 -  \item @{ML CodeUnit.const_of_cexpr}~@{text thy}~@{text "(constname, typ)"}
    1.48 -     maps a constant expression @{text "(constname, typ)"}
    1.49 -     to its canonical identifier.
    1.50 -
    1.51 -  \end{description}
    1.52 -*}
    1.53 -
    1.54  subsection {* Executable theory content: @{text Code} *}
    1.55  
    1.56  text {*
    1.57 @@ -1060,7 +1029,7 @@
    1.58    \begin{mldecls}
    1.59    @{index_ML Code.add_func: "bool -> thm -> theory -> theory"} \\
    1.60    @{index_ML Code.del_func: "thm -> theory -> theory"} \\
    1.61 -  @{index_ML Code.add_funcl: "CodeUnit.const * thm list Susp.T -> theory -> theory"} \\
    1.62 +  @{index_ML Code.add_funcl: "string * thm list Susp.T -> theory -> theory"} \\
    1.63    @{index_ML Code.add_inline: "thm -> theory -> theory"} \\
    1.64    @{index_ML Code.del_inline: "thm -> theory -> theory"} \\
    1.65    @{index_ML Code.add_inline_proc: "string * (theory -> cterm list -> thm list)
    1.66 @@ -1069,11 +1038,10 @@
    1.67    @{index_ML Code.add_preproc: "string * (theory -> thm list -> thm list)
    1.68      -> theory -> theory"} \\
    1.69    @{index_ML Code.del_preproc: "string -> theory -> theory"} \\
    1.70 -  @{index_ML Code.add_datatype: "string * ((string * sort) list * (string * typ list) list)
    1.71 -    -> theory -> theory"} \\
    1.72 +  @{index_ML Code.add_datatype: "(string * typ) list -> theory -> theory"} \\
    1.73    @{index_ML Code.get_datatype: "theory -> string
    1.74      -> (string * sort) list * (string * typ list) list"} \\
    1.75 -  @{index_ML Code.get_datatype_of_constr: "theory -> CodeUnit.const -> string option"}
    1.76 +  @{index_ML Code.get_datatype_of_constr: "theory -> string -> string option"}
    1.77    \end{mldecls}
    1.78  
    1.79    \begin{description}
    1.80 @@ -1113,12 +1081,9 @@
    1.81    \item @{ML Code.del_preproc}~@{text "name"}~@{text "thy"} removes
    1.82       generic preprcoessor named @{text name} from executable content.
    1.83  
    1.84 -  \item @{ML Code.add_datatype}~@{text "(name, spec)"}~@{text "thy"} adds
    1.85 -     a datatype to executable content, with type constructor
    1.86 -     @{text name} and specification @{text spec}; @{text spec} is
    1.87 -     a pair consisting of a list of type variable with sort
    1.88 -     constraints and a list of constructors with name
    1.89 -     and types of arguments.
    1.90 +  \item @{ML Code.add_datatype}~@{text cs}~@{text thy} adds
    1.91 +     a datatype to executable content, with generation
    1.92 +     set @{text cs}.
    1.93  
    1.94    \item @{ML Code.get_datatype_of_constr}~@{text "thy"}~@{text "const"}
    1.95       returns type constructor corresponding to
    1.96 @@ -1132,22 +1097,13 @@
    1.97  
    1.98  text %mlref {*
    1.99    \begin{mldecls}
   1.100 -  @{index_ML CodeUnit.const_ord: "CodeUnit.const * CodeUnit.const -> order"} \\
   1.101 -  @{index_ML CodeUnit.eq_const: "CodeUnit.const * CodeUnit.const -> bool"} \\
   1.102 -  @{index_ML CodeUnit.read_const: "theory -> string -> CodeUnit.const"} \\
   1.103 -  @{index_ML_structure CodeUnit.Consttab} \\
   1.104 -  @{index_ML CodeUnit.head_func: "thm -> CodeUnit.const * typ"} \\
   1.105 +  @{index_ML CodeUnit.read_const: "theory -> string -> string"} \\
   1.106 +  @{index_ML CodeUnit.head_func: "thm -> string * typ"} \\
   1.107    @{index_ML CodeUnit.rewrite_func: "thm list -> thm -> thm"} \\
   1.108    \end{mldecls}
   1.109  
   1.110    \begin{description}
   1.111  
   1.112 -  \item @{ML CodeUnit.const_ord},~@{ML CodeUnit.eq_const}
   1.113 -     provide order and equality on constant identifiers.
   1.114 -
   1.115 -  \item @{ML_struct CodeUnit.Consttab}
   1.116 -     provides table structures with constant identifiers as keys.
   1.117 -
   1.118    \item @{ML CodeUnit.read_const}~@{text thy}~@{text s}
   1.119       reads a constant as a concrete term expression @{text s}.
   1.120  
     2.1 --- a/doc-src/IsarAdvanced/Codegen/Thy/document/Codegen.tex	Fri Aug 24 14:14:16 2007 +0200
     2.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/document/Codegen.tex	Fri Aug 24 14:14:17 2007 +0200
     2.3 @@ -590,8 +590,6 @@
     2.4      \item[\isa{Pretty{\isacharunderscore}Char{\isacharunderscore}chr}] like \isa{Pretty{\isacharunderscore}Char},
     2.5         but also offers treatment of character codes; includes
     2.6         \isa{Pretty{\isacharunderscore}Int}.
     2.7 -    \item[\isa{Executable{\isacharunderscore}Set}] allows to generate code
     2.8 -       for finite sets using lists.
     2.9      \item[\isa{Executable{\isacharunderscore}Rat}] implements rational
    2.10         numbers.
    2.11      \item[\isa{Executable{\isacharunderscore}Real}] implements a subset of real numbers,
    2.12 @@ -1304,6 +1302,20 @@
    2.13    as constructor:%
    2.14  \end{isamarkuptext}%
    2.15  \isamarkuptrue%
    2.16 +\ %
    2.17 +\isadelimML
    2.18 +%
    2.19 +\endisadelimML
    2.20 +%
    2.21 +\isatagML
    2.22 +%
    2.23 +\endisatagML
    2.24 +{\isafoldML}%
    2.25 +%
    2.26 +\isadelimML
    2.27 +%
    2.28 +\endisadelimML
    2.29 +\isanewline
    2.30  \isacommand{code{\isacharunderscore}datatype}\isamarkupfalse%
    2.31  \ set\isanewline
    2.32  \isanewline
    2.33 @@ -1473,52 +1485,6 @@
    2.34  \end{isamarkuptext}%
    2.35  \isamarkuptrue%
    2.36  %
    2.37 -\isamarkupsubsection{Basics: \isa{CodeUnit}%
    2.38 -}
    2.39 -\isamarkuptrue%
    2.40 -%
    2.41 -\begin{isamarkuptext}%
    2.42 -This module provides identification of (probably overloaded)
    2.43 -  constants by unique identifiers.%
    2.44 -\end{isamarkuptext}%
    2.45 -\isamarkuptrue%
    2.46 -%
    2.47 -\isadelimmlref
    2.48 -%
    2.49 -\endisadelimmlref
    2.50 -%
    2.51 -\isatagmlref
    2.52 -%
    2.53 -\begin{isamarkuptext}%
    2.54 -\begin{mldecls}
    2.55 -  \indexmltype{CodeUnit.const}\verb|type CodeUnit.const = string * string option| \\
    2.56 -  \indexml{CodeUnit.const-of-cexpr}\verb|CodeUnit.const_of_cexpr: theory -> string * typ -> CodeUnit.const| \\
    2.57 - \end{mldecls}
    2.58 -
    2.59 -  \begin{description}
    2.60 -
    2.61 -  \item \verb|CodeUnit.const| is the identifier type:
    2.62 -     the product of a \emph{string} with a list of \emph{typs}.
    2.63 -     The \emph{string} is the constant name as represented inside Isabelle;
    2.64 -     for overloaded constants, the attached \emph{string option}
    2.65 -     is either \isa{SOME} type constructor denoting an instance,
    2.66 -     or \isa{NONE} for the polymorphic constant.
    2.67 -
    2.68 -  \item \verb|CodeUnit.const_of_cexpr|~\isa{thy}~\isa{{\isacharparenleft}constname{\isacharcomma}\ typ{\isacharparenright}}
    2.69 -     maps a constant expression \isa{{\isacharparenleft}constname{\isacharcomma}\ typ{\isacharparenright}}
    2.70 -     to its canonical identifier.
    2.71 -
    2.72 -  \end{description}%
    2.73 -\end{isamarkuptext}%
    2.74 -\isamarkuptrue%
    2.75 -%
    2.76 -\endisatagmlref
    2.77 -{\isafoldmlref}%
    2.78 -%
    2.79 -\isadelimmlref
    2.80 -%
    2.81 -\endisadelimmlref
    2.82 -%
    2.83  \isamarkupsubsection{Executable theory content: \isa{Code}%
    2.84  }
    2.85  \isamarkuptrue%
    2.86 @@ -1543,7 +1509,7 @@
    2.87  \begin{mldecls}
    2.88    \indexml{Code.add-func}\verb|Code.add_func: bool -> thm -> theory -> theory| \\
    2.89    \indexml{Code.del-func}\verb|Code.del_func: thm -> theory -> theory| \\
    2.90 -  \indexml{Code.add-funcl}\verb|Code.add_funcl: CodeUnit.const * thm list Susp.T -> theory -> theory| \\
    2.91 +  \indexml{Code.add-funcl}\verb|Code.add_funcl: string * thm list Susp.T -> theory -> theory| \\
    2.92    \indexml{Code.add-inline}\verb|Code.add_inline: thm -> theory -> theory| \\
    2.93    \indexml{Code.del-inline}\verb|Code.del_inline: thm -> theory -> theory| \\
    2.94    \indexml{Code.add-inline-proc}\verb|Code.add_inline_proc: string * (theory -> cterm list -> thm list)|\isasep\isanewline%
    2.95 @@ -1552,11 +1518,10 @@
    2.96    \indexml{Code.add-preproc}\verb|Code.add_preproc: string * (theory -> thm list -> thm list)|\isasep\isanewline%
    2.97  \verb|    -> theory -> theory| \\
    2.98    \indexml{Code.del-preproc}\verb|Code.del_preproc: string -> theory -> theory| \\
    2.99 -  \indexml{Code.add-datatype}\verb|Code.add_datatype: string * ((string * sort) list * (string * typ list) list)|\isasep\isanewline%
   2.100 -\verb|    -> theory -> theory| \\
   2.101 +  \indexml{Code.add-datatype}\verb|Code.add_datatype: (string * typ) list -> theory -> theory| \\
   2.102    \indexml{Code.get-datatype}\verb|Code.get_datatype: theory -> string|\isasep\isanewline%
   2.103  \verb|    -> (string * sort) list * (string * typ list) list| \\
   2.104 -  \indexml{Code.get-datatype-of-constr}\verb|Code.get_datatype_of_constr: theory -> CodeUnit.const -> string option|
   2.105 +  \indexml{Code.get-datatype-of-constr}\verb|Code.get_datatype_of_constr: theory -> string -> string option|
   2.106    \end{mldecls}
   2.107  
   2.108    \begin{description}
   2.109 @@ -1596,12 +1561,9 @@
   2.110    \item \verb|Code.del_preproc|~\isa{name}~\isa{thy} removes
   2.111       generic preprcoessor named \isa{name} from executable content.
   2.112  
   2.113 -  \item \verb|Code.add_datatype|~\isa{{\isacharparenleft}name{\isacharcomma}\ spec{\isacharparenright}}~\isa{thy} adds
   2.114 -     a datatype to executable content, with type constructor
   2.115 -     \isa{name} and specification \isa{spec}; \isa{spec} is
   2.116 -     a pair consisting of a list of type variable with sort
   2.117 -     constraints and a list of constructors with name
   2.118 -     and types of arguments.
   2.119 +  \item \verb|Code.add_datatype|~\isa{cs}~\isa{thy} adds
   2.120 +     a datatype to executable content, with generation
   2.121 +     set \isa{cs}.
   2.122  
   2.123    \item \verb|Code.get_datatype_of_constr|~\isa{thy}~\isa{const}
   2.124       returns type constructor corresponding to
   2.125 @@ -1631,22 +1593,13 @@
   2.126  %
   2.127  \begin{isamarkuptext}%
   2.128  \begin{mldecls}
   2.129 -  \indexml{CodeUnit.const-ord}\verb|CodeUnit.const_ord: CodeUnit.const * CodeUnit.const -> order| \\
   2.130 -  \indexml{CodeUnit.eq-const}\verb|CodeUnit.eq_const: CodeUnit.const * CodeUnit.const -> bool| \\
   2.131 -  \indexml{CodeUnit.read-const}\verb|CodeUnit.read_const: theory -> string -> CodeUnit.const| \\
   2.132 -  \indexmlstructure{CodeUnit.Consttab}\verb|structure CodeUnit.Consttab| \\
   2.133 -  \indexml{CodeUnit.head-func}\verb|CodeUnit.head_func: thm -> CodeUnit.const * typ| \\
   2.134 +  \indexml{CodeUnit.read-const}\verb|CodeUnit.read_const: theory -> string -> string| \\
   2.135 +  \indexml{CodeUnit.head-func}\verb|CodeUnit.head_func: thm -> string * typ| \\
   2.136    \indexml{CodeUnit.rewrite-func}\verb|CodeUnit.rewrite_func: thm list -> thm -> thm| \\
   2.137    \end{mldecls}
   2.138  
   2.139    \begin{description}
   2.140  
   2.141 -  \item \verb|CodeUnit.const_ord|,~\verb|CodeUnit.eq_const|
   2.142 -     provide order and equality on constant identifiers.
   2.143 -
   2.144 -  \item \verb|CodeUnit.Consttab|
   2.145 -     provides table structures with constant identifiers as keys.
   2.146 -
   2.147    \item \verb|CodeUnit.read_const|~\isa{thy}~\isa{s}
   2.148       reads a constant as a concrete term expression \isa{s}.
   2.149  
     3.1 --- a/doc-src/IsarAdvanced/Codegen/Thy/examples/Codegen.hs	Fri Aug 24 14:14:16 2007 +0200
     3.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/Codegen.hs	Fri Aug 24 14:14:17 2007 +0200
     3.3 @@ -10,11 +10,8 @@
     3.4  heada (x : xs) = x;
     3.5  heada [] = Codegen.nulla;
     3.6  
     3.7 -null_option :: Maybe a;
     3.8 -null_option = Nothing;
     3.9 -
    3.10  instance Codegen.Null (Maybe b) where {
    3.11 -  nulla = Codegen.null_option;
    3.12 +  nulla = Nothing;
    3.13  };
    3.14  
    3.15  dummy :: Maybe Nat.Nat;
     4.1 --- a/doc-src/IsarAdvanced/Codegen/Thy/examples/bool_infix.ML	Fri Aug 24 14:14:16 2007 +0200
     4.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/bool_infix.ML	Fri Aug 24 14:14:17 2007 +0200
     4.3 @@ -1,7 +1,7 @@
     4.4  structure Nat = 
     4.5  struct
     4.6  
     4.7 -datatype nat = Zero_nat | Suc of nat;
     4.8 +datatype nat = Suc of nat | Zero_nat;
     4.9  
    4.10  fun less_nat n (Suc m) = less_eq_nat n m
    4.11    | less_nat n Zero_nat = false
     5.1 --- a/doc-src/IsarAdvanced/Codegen/Thy/examples/bool_literal.ML	Fri Aug 24 14:14:16 2007 +0200
     5.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/bool_literal.ML	Fri Aug 24 14:14:17 2007 +0200
     5.3 @@ -1,7 +1,7 @@
     5.4  structure HOL = 
     5.5  struct
     5.6  
     5.7 -datatype boola = True | False;
     5.8 +datatype boola = False | True;
     5.9  
    5.10  fun anda x True = x
    5.11    | anda x False = False
    5.12 @@ -13,7 +13,7 @@
    5.13  structure Nat = 
    5.14  struct
    5.15  
    5.16 -datatype nat = Zero_nat | Suc of nat;
    5.17 +datatype nat = Suc of nat | Zero_nat;
    5.18  
    5.19  fun less_nat n (Suc m) = less_eq_nat n m
    5.20    | less_nat n Zero_nat = HOL.False
     6.1 --- a/doc-src/IsarAdvanced/Codegen/Thy/examples/bool_mlbool.ML	Fri Aug 24 14:14:16 2007 +0200
     6.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/bool_mlbool.ML	Fri Aug 24 14:14:17 2007 +0200
     6.3 @@ -1,7 +1,7 @@
     6.4  structure Nat = 
     6.5  struct
     6.6  
     6.7 -datatype nat = Zero_nat | Suc of nat;
     6.8 +datatype nat = Suc of nat | Zero_nat;
     6.9  
    6.10  fun less_nat n (Suc m) = less_eq_nat n m
    6.11    | less_nat n Zero_nat = false
     7.1 --- a/doc-src/IsarAdvanced/Codegen/Thy/examples/class.ML	Fri Aug 24 14:14:16 2007 +0200
     7.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/class.ML	Fri Aug 24 14:14:17 2007 +0200
     7.3 @@ -1,7 +1,7 @@
     7.4  structure Nat = 
     7.5  struct
     7.6  
     7.7 -datatype nat = Zero_nat | Suc of nat;
     7.8 +datatype nat = Suc of nat | Zero_nat;
     7.9  
    7.10  end; (*struct Nat*)
    7.11  
    7.12 @@ -14,11 +14,9 @@
    7.13  fun head B_ (x :: xs) = x
    7.14    | head B_ [] = null B_;
    7.15  
    7.16 -val null_option : 'a option = NONE;
    7.17 -
    7.18 -fun null_optiona () = {null = null_option} : ('b option) null;
    7.19 +fun null_option () = {null = NONE} : ('b option) null;
    7.20  
    7.21  val dummy : Nat.nat option =
    7.22 -  head (null_optiona ()) [SOME (Nat.Suc Nat.Zero_nat), NONE];
    7.23 +  head (null_option ()) [SOME (Nat.Suc Nat.Zero_nat), NONE];
    7.24  
    7.25  end; (*struct Codegen*)
     8.1 --- a/doc-src/IsarAdvanced/Codegen/Thy/examples/class.ocaml	Fri Aug 24 14:14:16 2007 +0200
     8.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/class.ocaml	Fri Aug 24 14:14:17 2007 +0200
     8.3 @@ -1,7 +1,7 @@
     8.4  module Nat = 
     8.5  struct
     8.6  
     8.7 -type nat = Zero_nat | Suc of nat;;
     8.8 +type nat = Suc of nat | Zero_nat;;
     8.9  
    8.10  end;; (*struct Nat*)
    8.11  
    8.12 @@ -14,11 +14,9 @@
    8.13  let rec head _B = function x :: xs -> x
    8.14                    | [] -> null _B;;
    8.15  
    8.16 -let rec null_option = None;;
    8.17 -
    8.18 -let null_optiona () = ({null = null_option} : ('b option) null);;
    8.19 +let null_option () = ({null = None} : ('b option) null);;
    8.20  
    8.21  let rec dummy
    8.22 -  = head (null_optiona ()) [Some (Nat.Suc Nat.Zero_nat); None];;
    8.23 +  = head (null_option ()) [Some (Nat.Suc Nat.Zero_nat); None];;
    8.24  
    8.25  end;; (*struct Codegen*)
     9.1 --- a/doc-src/IsarAdvanced/Codegen/Thy/examples/collect_duplicates.ML	Fri Aug 24 14:14:16 2007 +0200
     9.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/collect_duplicates.ML	Fri Aug 24 14:14:17 2007 +0200
     9.3 @@ -1,15 +1,15 @@
     9.4  structure HOL = 
     9.5  struct
     9.6  
     9.7 -type 'a eq = {eq : 'a -> 'a -> bool};
     9.8 -fun eq (A_:'a eq) = #eq A_;
     9.9 +type 'a eq = {eqop : 'a -> 'a -> bool};
    9.10 +fun eqop (A_:'a eq) = #eqop A_;
    9.11  
    9.12  end; (*struct HOL*)
    9.13  
    9.14  structure List = 
    9.15  struct
    9.16  
    9.17 -fun member A_ x (y :: ys) = HOL.eq A_ x y orelse member A_ x ys
    9.18 +fun member A_ x (y :: ys) = HOL.eqop A_ x y orelse member A_ x ys
    9.19    | member A_ x [] = false;
    9.20  
    9.21  end; (*struct List*)
    10.1 --- a/doc-src/IsarAdvanced/Codegen/Thy/examples/fac.ML	Fri Aug 24 14:14:16 2007 +0200
    10.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/fac.ML	Fri Aug 24 14:14:17 2007 +0200
    10.3 @@ -1,7 +1,7 @@
    10.4  structure Nat = 
    10.5  struct
    10.6  
    10.7 -datatype nat = Zero_nat | Suc of nat;
    10.8 +datatype nat = Suc of nat | Zero_nat;
    10.9  
   10.10  fun plus_nat (Suc m) n = plus_nat m (Suc n)
   10.11    | plus_nat Zero_nat n = n;
    11.1 --- a/doc-src/IsarAdvanced/Codegen/Thy/examples/fac_case.ML	Fri Aug 24 14:14:16 2007 +0200
    11.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/fac_case.ML	Fri Aug 24 14:14:17 2007 +0200
    11.3 @@ -1,7 +1,7 @@
    11.4  structure Nat = 
    11.5  struct
    11.6  
    11.7 -datatype nat = Zero_nat | Suc of nat;
    11.8 +datatype nat = Suc of nat | Zero_nat;
    11.9  
   11.10  fun nat_case f1 f2 Zero_nat = f1
   11.11    | nat_case f1 f2 (Suc nat) = f2 nat;
    12.1 --- a/doc-src/IsarAdvanced/Codegen/Thy/examples/lexicographic.ML	Fri Aug 24 14:14:16 2007 +0200
    12.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/lexicographic.ML	Fri Aug 24 14:14:17 2007 +0200
    12.3 @@ -1,8 +1,8 @@
    12.4  structure HOL = 
    12.5  struct
    12.6  
    12.7 -type 'a eq = {eq : 'a -> 'a -> bool};
    12.8 -fun eq (A_:'a eq) = #eq A_;
    12.9 +type 'a eq = {eqop : 'a -> 'a -> bool};
   12.10 +fun eqop (A_:'a eq) = #eqop A_;
   12.11  
   12.12  type 'a ord = {less_eq : 'a -> 'a -> bool, less : 'a -> 'a -> bool};
   12.13  fun less_eq (A_:'a ord) = #less_eq A_;
   12.14 @@ -13,7 +13,8 @@
   12.15  structure Codegen = 
   12.16  struct
   12.17  
   12.18 -fun less_eq_product (A1_, A2_) B_ (x1, y1) (x2, y2) =
   12.19 -  HOL.less A2_ x1 x2 orelse HOL.eq A1_ x1 x2 andalso HOL.less_eq B_ y1 y2;
   12.20 +fun less_eq (A1_, A2_) B_ (x1, y1) (x2, y2) =
   12.21 +  HOL.less A2_ x1 x2 orelse
   12.22 +    HOL.eqop A1_ x1 x2 andalso HOL.less_eq B_ y1 y2;
   12.23  
   12.24  end; (*struct Codegen*)
    13.1 --- a/doc-src/IsarAdvanced/Codegen/Thy/examples/monotype.ML	Fri Aug 24 14:14:16 2007 +0200
    13.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/monotype.ML	Fri Aug 24 14:14:17 2007 +0200
    13.3 @@ -1,12 +1,12 @@
    13.4  structure Nat = 
    13.5  struct
    13.6  
    13.7 -datatype nat = Zero_nat | Suc of nat;
    13.8 +datatype nat = Suc of nat | Zero_nat;
    13.9  
   13.10 -fun eq_nat Zero_nat (Suc m) = false
   13.11 -  | eq_nat (Suc n) Zero_nat = false
   13.12 -  | eq_nat (Suc n) (Suc m) = eq_nat n m
   13.13 -  | eq_nat Zero_nat Zero_nat = true;
   13.14 +fun eqop_nat Zero_nat (Suc m) = false
   13.15 +  | eqop_nat (Suc n) Zero_nat = false
   13.16 +  | eqop_nat (Suc n) (Suc m) = eqop_nat n m
   13.17 +  | eqop_nat Zero_nat Zero_nat = true;
   13.18  
   13.19  fun plus_nat (Suc m) n = plus_nat m (Suc n)
   13.20    | plus_nat Zero_nat n = n;
   13.21 @@ -39,7 +39,7 @@
   13.22    | list_all2 p xs [] = null xs
   13.23    | list_all2 p [] ys = null ys
   13.24    | list_all2 p xs ys =
   13.25 -    Nat.eq_nat (size_list xs) (size_list ys) andalso
   13.26 +    Nat.eqop_nat (size_list xs) (size_list ys) andalso
   13.27        list_all (fn a as (aa, b) => p aa b) (zip xs ys);
   13.28  
   13.29  end; (*struct List*)
   13.30 @@ -49,8 +49,8 @@
   13.31  
   13.32  datatype monotype = Mono of Nat.nat * monotype list;
   13.33  
   13.34 -fun eq_monotype (Mono (tyco1, typargs1)) (Mono (tyco2, typargs2)) =
   13.35 -  Nat.eq_nat tyco1 tyco2 andalso
   13.36 -    List.list_all2 eq_monotype typargs1 typargs2;
   13.37 +fun eqop_monotype (Mono (tyco1, typargs1)) (Mono (tyco2, typargs2)) =
   13.38 +  Nat.eqop_nat tyco1 tyco2 andalso
   13.39 +    List.list_all2 eqop_monotype typargs1 typargs2;
   13.40  
   13.41  end; (*struct Codegen*)
    14.1 --- a/doc-src/IsarAdvanced/Codegen/Thy/examples/pick1.ML	Fri Aug 24 14:14:16 2007 +0200
    14.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/pick1.ML	Fri Aug 24 14:14:17 2007 +0200
    14.3 @@ -8,7 +8,7 @@
    14.4  structure Nat = 
    14.5  struct
    14.6  
    14.7 -datatype nat = Zero_nat | Suc of nat;
    14.8 +datatype nat = Suc of nat | Zero_nat;
    14.9  
   14.10  fun less_nat n (Suc m) = less_eq_nat n m
   14.11    | less_nat n Zero_nat = false
    15.1 --- a/doc-src/IsarAdvanced/Codegen/Thy/examples/pick2.ML	Fri Aug 24 14:14:16 2007 +0200
    15.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/pick2.ML	Fri Aug 24 14:14:17 2007 +0200
    15.3 @@ -1,7 +1,7 @@
    15.4  structure Nat = 
    15.5  struct
    15.6  
    15.7 -datatype nat = Zero_nat | Suc of nat;
    15.8 +datatype nat = Suc of nat | Zero_nat;
    15.9  
   15.10  fun less_nat n (Suc m) = less_eq_nat n m
   15.11    | less_nat n Zero_nat = false
    16.1 --- a/doc-src/IsarAdvanced/Codegen/Thy/examples/set_list.ML	Fri Aug 24 14:14:16 2007 +0200
    16.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/set_list.ML	Fri Aug 24 14:14:17 2007 +0200
    16.3 @@ -1,8 +1,8 @@
    16.4  structure HOL = 
    16.5  struct
    16.6  
    16.7 -type 'a eq = {eq : 'a -> 'a -> bool};
    16.8 -fun eq (A_:'a eq) = #eq A_;
    16.9 +type 'a eq = {eqop : 'a -> 'a -> bool};
   16.10 +fun eqop (A_:'a eq) = #eqop A_;
   16.11  
   16.12  end; (*struct HOL*)
   16.13  
   16.14 @@ -12,7 +12,7 @@
   16.15  fun foldr f (x :: xs) a = f x (foldr f xs a)
   16.16    | foldr f [] a = a;
   16.17  
   16.18 -fun member A_ x (y :: ys) = HOL.eq A_ x y orelse member A_ x ys
   16.19 +fun member A_ x (y :: ys) = HOL.eqop A_ x y orelse member A_ x ys
   16.20    | member A_ x [] = false;
   16.21  
   16.22  end; (*struct List*)
   16.23 @@ -26,10 +26,10 @@
   16.24  
   16.25  fun insert x (Set xs) = Set (x :: xs);
   16.26  
   16.27 -fun uniona xs (Set ys) = List.foldr insert ys xs;
   16.28 -
   16.29 -fun union (Set xs) = List.foldr uniona xs empty;
   16.30 +fun union xs (Set ys) = List.foldr insert ys xs;
   16.31  
   16.32  fun member A_ x (Set xs) = List.member A_ x xs;
   16.33  
   16.34 +fun uniona (Set xs) = List.foldr union xs empty;
   16.35 +
   16.36  end; (*struct Set*)
    17.1 --- a/doc-src/IsarAdvanced/Codegen/Thy/examples/tree.ML	Fri Aug 24 14:14:16 2007 +0200
    17.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/tree.ML	Fri Aug 24 14:14:17 2007 +0200
    17.3 @@ -1,8 +1,8 @@
    17.4  structure HOL = 
    17.5  struct
    17.6  
    17.7 -type 'a eq = {eq : 'a -> 'a -> bool};
    17.8 -fun eq (A_:'a eq) = #eq A_;
    17.9 +type 'a eq = {eqop : 'a -> 'a -> bool};
   17.10 +fun eqop (A_:'a eq) = #eqop A_;
   17.11  
   17.12  type 'a ord = {less_eq : 'a -> 'a -> bool, less : 'a -> 'a -> bool};
   17.13  fun less_eq (A_:'a ord) = #less_eq A_;
   17.14 @@ -24,14 +24,14 @@
   17.15  structure Nat = 
   17.16  struct
   17.17  
   17.18 -datatype nat = Zero_nat | Suc of nat;
   17.19 +datatype nat = Suc of nat | Zero_nat;
   17.20  
   17.21 -fun eq_nat Zero_nat (Suc m) = false
   17.22 -  | eq_nat (Suc n) Zero_nat = false
   17.23 -  | eq_nat (Suc n) (Suc m) = eq_nat n m
   17.24 -  | eq_nat Zero_nat Zero_nat = true;
   17.25 +fun eqop_nat Zero_nat (Suc m) = false
   17.26 +  | eqop_nat (Suc n) Zero_nat = false
   17.27 +  | eqop_nat (Suc n) (Suc m) = eqop_nat n m
   17.28 +  | eqop_nat Zero_nat Zero_nat = true;
   17.29  
   17.30 -val eq_nata = {eq = eq_nat} : nat HOL.eq;
   17.31 +val eq_nat = {eqop = eqop_nat} : nat HOL.eq;
   17.32  
   17.33  fun less_nat n (Suc m) = less_eq_nat n m
   17.34    | less_nat n Zero_nat = false
   17.35 @@ -50,8 +50,9 @@
   17.36  structure Codegen = 
   17.37  struct
   17.38  
   17.39 -datatype ('a, 'b) searchtree = Leaf of 'a * 'b |
   17.40 -  Branch of ('a, 'b) searchtree * 'a * ('a, 'b) searchtree;
   17.41 +datatype ('a, 'b) searchtree =
   17.42 +  Branch of ('a, 'b) searchtree * 'a * ('a, 'b) searchtree |
   17.43 +  Leaf of 'a * 'b;
   17.44  
   17.45  fun update (C1_, C2_) (it, entry) (Branch (t1, key, t2)) =
   17.46    (if HOL.less_eq ((Orderings.ord_order o Orderings.order_linorder) C2_)
   17.47 @@ -59,7 +60,7 @@
   17.48      then Branch (update (C1_, C2_) (it, entry) t1, key, t2)
   17.49      else Branch (t1, key, update (C1_, C2_) (it, entry) t2))
   17.50    | update (C1_, C2_) (it, entry) (Leaf (key, vala)) =
   17.51 -    (if HOL.eq C1_ it key then Leaf (key, entry)
   17.52 +    (if HOL.eqop C1_ it key then Leaf (key, entry)
   17.53        else (if HOL.less_eq
   17.54                   ((Orderings.ord_order o Orderings.order_linorder) C2_) it
   17.55                   key
   17.56 @@ -67,13 +68,13 @@
   17.57               else Branch (Leaf (key, vala), it, Leaf (it, entry))));
   17.58  
   17.59  val example : (Nat.nat, (Nat.nat list)) searchtree =
   17.60 -  update (Nat.eq_nata, Nat.linorder_nat)
   17.61 +  update (Nat.eq_nat, Nat.linorder_nat)
   17.62      (Nat.Suc (Nat.Suc (Nat.Suc (Nat.Suc Nat.Zero_nat))),
   17.63        [Nat.Suc (Nat.Suc Nat.Zero_nat), Nat.Suc (Nat.Suc Nat.Zero_nat)])
   17.64 -    (update (Nat.eq_nata, Nat.linorder_nat)
   17.65 +    (update (Nat.eq_nat, Nat.linorder_nat)
   17.66        (Nat.Suc (Nat.Suc (Nat.Suc Nat.Zero_nat)),
   17.67          [Nat.Suc (Nat.Suc (Nat.Suc Nat.Zero_nat))])
   17.68 -      (update (Nat.eq_nata, Nat.linorder_nat)
   17.69 +      (update (Nat.eq_nat, Nat.linorder_nat)
   17.70          (Nat.Suc (Nat.Suc Nat.Zero_nat), [Nat.Suc (Nat.Suc Nat.Zero_nat)])
   17.71          (Leaf (Nat.Suc Nat.Zero_nat, []))));
   17.72