updated manual
authorhaftmann
Thu Jan 04 17:11:09 2007 +0100 (2007-01-04)
changeset 219934b802a9e0738
parent 21992 337990f42ce0
child 21994 dfa5133dbe73
updated manual
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/arbitrary.ML
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/collect_duplicates.ML
doc-src/IsarAdvanced/Codegen/Thy/examples/dirty_set.ML
doc-src/IsarAdvanced/Codegen/Thy/examples/fac.ML
doc-src/IsarAdvanced/Codegen/Thy/examples/fac_case.ML
doc-src/IsarAdvanced/Codegen/Thy/examples/integers.ML
doc-src/IsarAdvanced/Codegen/Thy/examples/lexicographic.ML
doc-src/IsarAdvanced/Codegen/Thy/examples/lookup.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	Thu Jan 04 15:29:44 2007 +0100
     1.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy	Thu Jan 04 17:11:09 2007 +0100
     1.3 @@ -182,7 +182,7 @@
     1.4  typedecl 'a foo
     1.5  
     1.6  definition
     1.7 -  bar :: "'a foo \<Rightarrow> 'a \<Rightarrow> 'a"
     1.8 +  bar :: "'a foo \<Rightarrow> 'a \<Rightarrow> 'a" where
     1.9    "bar x y = y"
    1.10  
    1.11  (*<*)
    1.12 @@ -194,7 +194,7 @@
    1.13  datatype 'a foo = Foo
    1.14  
    1.15  definition
    1.16 -  bar :: "'a foo \<Rightarrow> 'a \<Rightarrow> 'a"
    1.17 +  bar :: "'a foo \<Rightarrow> 'a \<Rightarrow> 'a" where
    1.18    "bar x y = y"
    1.19  (*>*)
    1.20  
    1.21 @@ -212,7 +212,7 @@
    1.22  (*>*)
    1.23  
    1.24  definition
    1.25 -  pick_some :: "'a list \<Rightarrow> 'a"
    1.26 +  pick_some :: "'a list \<Rightarrow> 'a" where
    1.27    "pick_some xs = (SOME x. x \<in> set xs)"
    1.28  
    1.29  (*<*)
    1.30 @@ -221,7 +221,7 @@
    1.31  setup {* Sign.parent_path *}
    1.32  
    1.33  definition
    1.34 -  pick_some :: "'a list \<Rightarrow> 'a"
    1.35 +  pick_some :: "'a list \<Rightarrow> 'a" where
    1.36    "pick_some = hd"
    1.37  (*>*)
    1.38  
    1.39 @@ -655,7 +655,7 @@
    1.40  *}
    1.41  
    1.42  definition
    1.43 -  double_inc :: "int \<Rightarrow> int"
    1.44 +  double_inc :: "int \<Rightarrow> int" where
    1.45    "double_inc k = 2 * k + 1"
    1.46  
    1.47  code_gen double_inc (SML "examples/integers.ML")
    1.48 @@ -745,11 +745,11 @@
    1.49  (*>*)
    1.50  
    1.51  axclass eq \<subseteq> type
    1.52 -  attach "op ="
    1.53 +  (attach "op =")
    1.54  
    1.55  text {*
    1.56    This merely introduces a class @{text eq} with corresponding
    1.57 -  operation @{const "op ="};
    1.58 +  operation @{text "op ="};
    1.59    the preprocessing framework does the rest.
    1.60  *}
    1.61  
    1.62 @@ -926,7 +926,7 @@
    1.63    (SML "![]" and infixl 7 "::")
    1.64  
    1.65  definition
    1.66 -  dummy_set :: "(nat \<Rightarrow> nat) set"
    1.67 +  dummy_set :: "(nat \<Rightarrow> nat) set" where
    1.68    "dummy_set = {Suc}"
    1.69  
    1.70  text {*
    1.71 @@ -946,7 +946,7 @@
    1.72  *}
    1.73  
    1.74  definition
    1.75 -  foobar_set :: "nat set"
    1.76 +  foobar_set :: "nat set" where
    1.77    "foobar_set = {0, 1, 2}"
    1.78  
    1.79  text {*
    1.80 @@ -1053,7 +1053,7 @@
    1.81  *}
    1.82  
    1.83  definition
    1.84 -  arbitrary_option :: "'a option"
    1.85 +  arbitrary_option :: "'a option" where
    1.86    [symmetric, code inline]: "arbitrary_option = arbitrary"
    1.87  
    1.88  text {*
     2.1 --- a/doc-src/IsarAdvanced/Codegen/Thy/document/Codegen.tex	Thu Jan 04 15:29:44 2007 +0100
     2.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/document/Codegen.tex	Thu Jan 04 17:11:09 2007 +0100
     2.3 @@ -225,7 +225,7 @@
     2.4  \isanewline
     2.5  \isacommand{definition}\isamarkupfalse%
     2.6  \isanewline
     2.7 -\ \ bar\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ foo\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequoteclose}\isanewline
     2.8 +\ \ bar\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ foo\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
     2.9  \ \ {\isachardoublequoteopen}bar\ x\ y\ {\isacharequal}\ y{\isachardoublequoteclose}\isanewline
    2.10  %
    2.11  \isadelimML
    2.12 @@ -266,7 +266,7 @@
    2.13  \endisadelimML
    2.14  \isacommand{definition}\isamarkupfalse%
    2.15  \isanewline
    2.16 -\ \ pick{\isacharunderscore}some\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequoteclose}\isanewline
    2.17 +\ \ pick{\isacharunderscore}some\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
    2.18  \ \ {\isachardoublequoteopen}pick{\isacharunderscore}some\ xs\ {\isacharequal}\ {\isacharparenleft}SOME\ x{\isachardot}\ x\ {\isasymin}\ set\ xs{\isacharparenright}{\isachardoublequoteclose}\isanewline
    2.19  %
    2.20  \isadelimML
    2.21 @@ -864,7 +864,7 @@
    2.22  \isamarkuptrue%
    2.23  \isacommand{definition}\isamarkupfalse%
    2.24  \isanewline
    2.25 -\ \ double{\isacharunderscore}inc\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}int\ {\isasymRightarrow}\ int{\isachardoublequoteclose}\isanewline
    2.26 +\ \ double{\isacharunderscore}inc\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}int\ {\isasymRightarrow}\ int{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
    2.27  \ \ {\isachardoublequoteopen}double{\isacharunderscore}inc\ k\ {\isacharequal}\ {\isadigit{2}}\ {\isacharasterisk}\ k\ {\isacharplus}\ {\isadigit{1}}{\isachardoublequoteclose}\isanewline
    2.28  \isanewline
    2.29  \isacommand{code{\isacharunderscore}gen}\isamarkupfalse%
    2.30 @@ -981,7 +981,7 @@
    2.31  \isanewline
    2.32  \isacommand{axclass}\isamarkupfalse%
    2.33  \ eq\ {\isasymsubseteq}\ type\isanewline
    2.34 -\ \ \isakeyword{attach}\ {\isachardoublequoteopen}op\ {\isacharequal}{\isachardoublequoteclose}%
    2.35 +\ \ {\isacharparenleft}\isakeyword{attach}\ {\isachardoublequoteopen}op\ {\isacharequal}{\isachardoublequoteclose}{\isacharparenright}%
    2.36  \begin{isamarkuptext}%
    2.37  This merely introduces a class \isa{eq} with corresponding
    2.38    operation \isa{foo{\isachardot}op\ {\isacharequal}};
    2.39 @@ -1351,7 +1351,7 @@
    2.40  \isanewline
    2.41  \isacommand{definition}\isamarkupfalse%
    2.42  \isanewline
    2.43 -\ \ dummy{\isacharunderscore}set\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}nat\ {\isasymRightarrow}\ nat{\isacharparenright}\ set{\isachardoublequoteclose}\isanewline
    2.44 +\ \ dummy{\isacharunderscore}set\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}nat\ {\isasymRightarrow}\ nat{\isacharparenright}\ set{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
    2.45  \ \ {\isachardoublequoteopen}dummy{\isacharunderscore}set\ {\isacharequal}\ {\isacharbraceleft}Suc{\isacharbraceright}{\isachardoublequoteclose}%
    2.46  \begin{isamarkuptext}%
    2.47  Then code generation for \isa{dummy{\isacharunderscore}set} will fail.
    2.48 @@ -1371,7 +1371,7 @@
    2.49  \isamarkuptrue%
    2.50  \isacommand{definition}\isamarkupfalse%
    2.51  \isanewline
    2.52 -\ \ foobar{\isacharunderscore}set\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ set{\isachardoublequoteclose}\isanewline
    2.53 +\ \ foobar{\isacharunderscore}set\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ set{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
    2.54  \ \ {\isachardoublequoteopen}foobar{\isacharunderscore}set\ {\isacharequal}\ {\isacharbraceleft}{\isadigit{0}}{\isacharcomma}\ {\isadigit{1}}{\isacharcomma}\ {\isadigit{2}}{\isacharbraceright}{\isachardoublequoteclose}%
    2.55  \begin{isamarkuptext}%
    2.56  In this case the serializer would complain that \isa{insert}
    2.57 @@ -1513,7 +1513,7 @@
    2.58  \isamarkuptrue%
    2.59  \isacommand{definition}\isamarkupfalse%
    2.60  \isanewline
    2.61 -\ \ arbitrary{\isacharunderscore}option\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ option{\isachardoublequoteclose}\isanewline
    2.62 +\ \ arbitrary{\isacharunderscore}option\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ option{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
    2.63  \ \ {\isacharbrackleft}symmetric{\isacharcomma}\ code\ inline{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}arbitrary{\isacharunderscore}option\ {\isacharequal}\ arbitrary{\isachardoublequoteclose}%
    2.64  \begin{isamarkuptext}%
    2.65  By that, we replace any \isa{arbitrary} with option type
     3.1 --- a/doc-src/IsarAdvanced/Codegen/Thy/examples/Codegen.hs	Thu Jan 04 15:29:44 2007 +0100
     3.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/Codegen.hs	Thu Jan 04 17:11:09 2007 +0100
     3.3 @@ -2,11 +2,10 @@
     3.4  import qualified Nat
     3.5  
     3.6  class Null a where
     3.7 -  null :: a
     3.8 +  nulla :: a
     3.9  
    3.10 -head :: (Codegen.Null a_1) => [a_1] -> a_1
    3.11 -head (y : xs) = y
    3.12 -head [] = Codegen.null
    3.13 +heada :: (Codegen.Null a) => ([a] -> a)
    3.14 +heada (y : xs) = y
    3.15  
    3.16  null_option :: Maybe b
    3.17  null_option = Nothing
    3.18 @@ -15,4 +14,4 @@
    3.19    null = Codegen.null_option
    3.20  
    3.21  dummy :: Maybe Nat.Nat
    3.22 -dummy = Codegen.head [Just (Nat.Suc Nat.Zero_nat), Nothing]
    3.23 +dummy = Codegen.heada [Just (Nat.Suc Nat.Zero_nat), Nothing]
     4.1 --- a/doc-src/IsarAdvanced/Codegen/Thy/examples/arbitrary.ML	Thu Jan 04 15:29:44 2007 +0100
     4.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/arbitrary.ML	Thu Jan 04 17:11:09 2007 +0100
     4.3 @@ -6,8 +6,7 @@
     4.4  
     4.5  val arbitrary_option : 'a option = NONE;
     4.6  
     4.7 -fun dummy_option [] = arbitrary_option
     4.8 -  | dummy_option (x :: xs) = SOME x;
     4.9 +fun dummy_option [] = arbitrary_option;
    4.10  
    4.11  end; (*struct Codegen*)
    4.12  
     5.1 --- a/doc-src/IsarAdvanced/Codegen/Thy/examples/bool_infix.ML	Thu Jan 04 15:29:44 2007 +0100
     5.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/bool_infix.ML	Thu Jan 04 17:11:09 2007 +0100
     5.3 @@ -4,8 +4,7 @@
     5.4  structure HOL = 
     5.5  struct
     5.6  
     5.7 -fun nota false = true
     5.8 -  | nota true = false;
     5.9 +fun nota false = true;
    5.10  
    5.11  end; (*struct HOL*)
    5.12  
    5.13 @@ -14,9 +13,7 @@
    5.14  
    5.15  datatype nat = Zero_nat | Suc of nat;
    5.16  
    5.17 -fun less_nat Zero_nat (Suc n) = true
    5.18 -  | less_nat n Zero_nat = false
    5.19 -  | less_nat (Suc m) (Suc n) = less_nat m n;
    5.20 +fun less_nat Zero_nat (Suc n) = true;
    5.21  
    5.22  fun less_eq_nat m n = HOL.nota (less_nat n m);
    5.23  
    5.24 @@ -25,7 +22,9 @@
    5.25  structure Codegen = 
    5.26  struct
    5.27  
    5.28 -fun in_interval (k, l) n = Nat.less_eq_nat k n andalso Nat.less_eq_nat n l;
    5.29 +fun in_interval (k, l) n = (Nat.less_eq_nat k n andalso Nat.less_eq_nat n l)
    5.30 +  | in_interval (k, l) n =
    5.31 +    (Nat.less_eq_nat k n andalso Nat.less_eq_nat n l);
    5.32  
    5.33  end; (*struct Codegen*)
    5.34  
     6.1 --- a/doc-src/IsarAdvanced/Codegen/Thy/examples/bool_literal.ML	Thu Jan 04 15:29:44 2007 +0100
     6.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/bool_literal.ML	Thu Jan 04 17:11:09 2007 +0100
     6.3 @@ -6,13 +6,9 @@
     6.4  
     6.5  datatype boola = True | False;
     6.6  
     6.7 -fun nota False = True
     6.8 -  | nota True = False;
     6.9 +fun nota False = True;
    6.10  
    6.11 -fun op_conj y True = y
    6.12 -  | op_conj x False = False
    6.13 -  | op_conj True y = y
    6.14 -  | op_conj False x = False;
    6.15 +fun op_conj y True = y;
    6.16  
    6.17  end; (*struct HOL*)
    6.18  
    6.19 @@ -21,9 +17,7 @@
    6.20  
    6.21  datatype nat = Zero_nat | Suc of nat;
    6.22  
    6.23 -fun less_nat Zero_nat (Suc n) = HOL.True
    6.24 -  | less_nat n Zero_nat = HOL.False
    6.25 -  | less_nat (Suc m) (Suc n) = less_nat m n;
    6.26 +fun less_nat Zero_nat (Suc n) = HOL.True;
    6.27  
    6.28  fun less_eq_nat m n = HOL.nota (less_nat n m);
    6.29  
    6.30 @@ -33,7 +27,9 @@
    6.31  struct
    6.32  
    6.33  fun in_interval (k, l) n =
    6.34 -  HOL.op_conj (Nat.less_eq_nat k n) (Nat.less_eq_nat n l);
    6.35 +  HOL.op_conj (Nat.less_eq_nat k n) (Nat.less_eq_nat n l)
    6.36 +  | in_interval (k, l) n =
    6.37 +    HOL.op_conj (Nat.less_eq_nat k n) (Nat.less_eq_nat n l);
    6.38  
    6.39  end; (*struct Codegen*)
    6.40  
     7.1 --- a/doc-src/IsarAdvanced/Codegen/Thy/examples/bool_mlbool.ML	Thu Jan 04 15:29:44 2007 +0100
     7.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/bool_mlbool.ML	Thu Jan 04 17:11:09 2007 +0100
     7.3 @@ -4,8 +4,7 @@
     7.4  structure HOL = 
     7.5  struct
     7.6  
     7.7 -fun nota false = true
     7.8 -  | nota true = false;
     7.9 +fun nota false = true;
    7.10  
    7.11  end; (*struct HOL*)
    7.12  
    7.13 @@ -14,9 +13,7 @@
    7.14  
    7.15  datatype nat = Zero_nat | Suc of nat;
    7.16  
    7.17 -fun less_nat Zero_nat (Suc n) = true
    7.18 -  | less_nat n Zero_nat = false
    7.19 -  | less_nat (Suc m) (Suc n) = less_nat m n;
    7.20 +fun less_nat Zero_nat (Suc n) = true;
    7.21  
    7.22  fun less_eq_nat m n = HOL.nota (less_nat n m);
    7.23  
    7.24 @@ -26,7 +23,9 @@
    7.25  struct
    7.26  
    7.27  fun in_interval (k, l) n =
    7.28 -  (Nat.less_eq_nat k n) andalso (Nat.less_eq_nat n l);
    7.29 +  (Nat.less_eq_nat k n) andalso (Nat.less_eq_nat n l)
    7.30 +  | in_interval (k, l) n =
    7.31 +    (Nat.less_eq_nat k n) andalso (Nat.less_eq_nat n l);
    7.32  
    7.33  end; (*struct Codegen*)
    7.34  
     8.1 --- a/doc-src/IsarAdvanced/Codegen/Thy/examples/class.ML	Thu Jan 04 15:29:44 2007 +0100
     8.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/class.ML	Thu Jan 04 17:11:09 2007 +0100
     8.3 @@ -14,12 +14,11 @@
     8.4  type 'a null = {null_ : 'a};
     8.5  fun null (A_:'a null) = #null_ A_;
     8.6  
     8.7 -fun head (A_1_:'a_1 null) (y :: xs) = y
     8.8 -  | head (A_1_:'a_1 null) [] = null A_1_;
     8.9 +fun head (A_:'a null) (y :: xs) = y;
    8.10  
    8.11  val null_option : 'b option = NONE;
    8.12  
    8.13 -fun null_optiona () = {null_ = null_option} : ('b option) null
    8.14 +fun null_optiona () = {null_ = null_option} : ('b option) null ;;
    8.15  
    8.16  val dummy : Nat.nat option =
    8.17    head (null_optiona ()) [SOME (Nat.Suc Nat.Zero_nat), NONE];
     9.1 --- a/doc-src/IsarAdvanced/Codegen/Thy/examples/collect_duplicates.ML	Thu Jan 04 15:29:44 2007 +0100
     9.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/collect_duplicates.ML	Thu Jan 04 17:11:09 2007 +0100
     9.3 @@ -12,9 +12,8 @@
     9.4  structure List = 
     9.5  struct
     9.6  
     9.7 -fun memberl (A_1_:'a_1 Code_Generator.eq) x (y :: ys) =
     9.8 -  Code_Generator.op_eq A_1_ x y orelse memberl A_1_ x ys
     9.9 -  | memberl (A_1_:'a_1 Code_Generator.eq) x [] = false;
    9.10 +fun memberl (A_:'a Code_Generator.eq) x (y :: ys) =
    9.11 +  (Code_Generator.op_eq A_ x y orelse memberl A_ x ys);
    9.12  
    9.13  end; (*struct List*)
    9.14  
    9.15 @@ -25,8 +24,7 @@
    9.16    (if List.memberl A_ z xs
    9.17      then (if List.memberl A_ z ys then collect_duplicates A_ xs ys zs
    9.18             else collect_duplicates A_ xs (z :: ys) zs)
    9.19 -    else collect_duplicates A_ (z :: xs) (z :: ys) zs)
    9.20 -  | collect_duplicates (A_:'a Code_Generator.eq) y ys [] = y;
    9.21 +    else collect_duplicates A_ (z :: xs) (z :: ys) zs);
    9.22  
    9.23  end; (*struct Codegen*)
    9.24  
    10.1 --- a/doc-src/IsarAdvanced/Codegen/Thy/examples/dirty_set.ML	Thu Jan 04 15:29:44 2007 +0100
    10.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/dirty_set.ML	Thu Jan 04 17:11:09 2007 +0100
    10.3 @@ -11,11 +11,11 @@
    10.4  structure Codegen = 
    10.5  struct
    10.6  
    10.7 -val dummy_set : (Nat.nat -> Nat.nat) list = Nat.Suc :: [];
    10.8 +val dummy_set : (Nat.nat -> Nat.nat) list = (Nat.Suc :: []);
    10.9  
   10.10  val foobar_set : Nat.nat list =
   10.11 -  Nat.Zero_nat ::
   10.12 -    (Nat.Suc Nat.Zero_nat :: (Nat.Suc (Nat.Suc Nat.Zero_nat) :: []));
   10.13 +  (Nat.Zero_nat ::
   10.14 +    (Nat.Suc Nat.Zero_nat :: (Nat.Suc (Nat.Suc Nat.Zero_nat) :: [])));
   10.15  
   10.16  end; (*struct Codegen*)
   10.17  
    11.1 --- a/doc-src/IsarAdvanced/Codegen/Thy/examples/fac.ML	Thu Jan 04 15:29:44 2007 +0100
    11.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/fac.ML	Thu Jan 04 17:11:09 2007 +0100
    11.3 @@ -7,18 +7,16 @@
    11.4  datatype nat = Zero_nat | Suc of nat;
    11.5  
    11.6  fun plus_nat (Suc m) n = plus_nat m (Suc n)
    11.7 -  | plus_nat Zero_nat y = y;
    11.8 +  | plus_nat (Suc m) n = Suc (plus_nat m n);
    11.9  
   11.10 -fun times_nat (Suc m) n = plus_nat n (times_nat m n)
   11.11 -  | times_nat Zero_nat n = Zero_nat;
   11.12 +fun times_nat (Suc m) n = plus_nat n (times_nat m n);
   11.13  
   11.14  end; (*struct Nat*)
   11.15  
   11.16  structure Codegen = 
   11.17  struct
   11.18  
   11.19 -fun fac (Nat.Suc n) = Nat.times_nat (Nat.Suc n) (fac n)
   11.20 -  | fac Nat.Zero_nat = Nat.Suc Nat.Zero_nat;
   11.21 +fun fac (Nat.Suc n) = Nat.times_nat (Nat.Suc n) (fac n);
   11.22  
   11.23  end; (*struct Codegen*)
   11.24  
    12.1 --- a/doc-src/IsarAdvanced/Codegen/Thy/examples/fac_case.ML	Thu Jan 04 15:29:44 2007 +0100
    12.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/fac_case.ML	Thu Jan 04 17:11:09 2007 +0100
    12.3 @@ -7,10 +7,9 @@
    12.4  datatype nat = Zero_nat | Suc of nat;
    12.5  
    12.6  fun plus_nat (Suc m) n = plus_nat m (Suc n)
    12.7 -  | plus_nat Zero_nat y = y;
    12.8 +  | plus_nat (Suc m) n = Suc (plus_nat m n);
    12.9  
   12.10 -fun times_nat (Suc m) n = plus_nat n (times_nat m n)
   12.11 -  | times_nat Zero_nat n = Zero_nat;
   12.12 +fun times_nat (Suc m) n = plus_nat n (times_nat m n);
   12.13  
   12.14  end; (*struct Nat*)
   12.15  
   12.16 @@ -19,7 +18,8 @@
   12.17  
   12.18  fun fac n =
   12.19    (case n of Nat.Zero_nat => Nat.Suc Nat.Zero_nat
   12.20 -     | Nat.Suc ma => Nat.times_nat n (fac ma));
   12.21 +     | Nat.Suc m => Nat.times_nat n (fac m))
   12.22 +  | fac (Nat.Suc n) = Nat.times_nat (Nat.Suc n) (fac n);
   12.23  
   12.24  end; (*struct Codegen*)
   12.25  
    13.1 --- a/doc-src/IsarAdvanced/Codegen/Thy/examples/integers.ML	Thu Jan 04 15:29:44 2007 +0100
    13.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/integers.ML	Thu Jan 04 17:11:09 2007 +0100
    13.3 @@ -4,8 +4,8 @@
    13.4  structure Codegen = 
    13.5  struct
    13.6  
    13.7 -fun double_inc a =
    13.8 -  IntInf.+ ((IntInf.* ((2 : IntInf.int), a)), (1 : IntInf.int));
    13.9 +val double_inc : IntInf.int -> IntInf.int =
   13.10 +  (fn k => IntInf.+ ((IntInf.* ((2 : IntInf.int), k)), (1 : IntInf.int)));
   13.11  
   13.12  end; (*struct Codegen*)
   13.13  
    14.1 --- a/doc-src/IsarAdvanced/Codegen/Thy/examples/lexicographic.ML	Thu Jan 04 15:29:44 2007 +0100
    14.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/lexicographic.ML	Thu Jan 04 17:11:09 2007 +0100
    14.3 @@ -14,7 +14,7 @@
    14.4  
    14.5  fun op_eq_prod (A_:'a Code_Generator.eq) (B_:'b Code_Generator.eq) (x1, y1)
    14.6    (x2, y2) =
    14.7 -  Code_Generator.op_eq A_ x1 x2 andalso Code_Generator.op_eq B_ y1 y2;
    14.8 +  (Code_Generator.op_eq A_ x1 x2 andalso Code_Generator.op_eq B_ y1 y2);
    14.9  
   14.10  end; (*struct Product_Type*)
   14.11  
   14.12 @@ -33,18 +33,18 @@
   14.13  fun less_prod (B_:'b Code_Generator.eq * 'b Orderings.ord)
   14.14    (C_:'c Code_Generator.eq * 'c Orderings.ord) p1 p2 =
   14.15    let
   14.16 -    val (x1a, y1a) = p1;
   14.17 -    val (x2a, y2a) = p2;
   14.18 +    val (x1, y1) = p1;
   14.19 +    val (x2, y2) = p2;
   14.20    in
   14.21 -    Orderings.less (#2 B_) x1a x2a orelse
   14.22 -      Code_Generator.op_eq (#1 B_) x1a x2a andalso
   14.23 -        Orderings.less (#2 C_) y1a y2a
   14.24 +    (Orderings.less (#2 B_) x1 x2 orelse
   14.25 +      Code_Generator.op_eq (#1 B_) x1 x2 andalso
   14.26 +        Orderings.less (#2 C_) y1 y2)
   14.27    end;
   14.28  
   14.29  fun less_eq_prod (B_:'b Code_Generator.eq * 'b Orderings.ord)
   14.30    (C_:'c Code_Generator.eq * 'c Orderings.ord) p1 p2 =
   14.31 -  less_prod ((#1 B_), (#2 B_)) ((#1 C_), (#2 C_)) p1 p2 orelse
   14.32 -    Product_Type.op_eq_prod (#1 B_) (#1 C_) p1 p2;
   14.33 +  (less_prod ((#1 B_), (#2 B_)) ((#1 C_), (#2 C_)) p1 p2 orelse
   14.34 +    Product_Type.op_eq_prod (#1 B_) (#1 C_) p1 p2);
   14.35  
   14.36  end; (*struct Codegen*)
   14.37  
    15.1 --- a/doc-src/IsarAdvanced/Codegen/Thy/examples/lookup.ML	Thu Jan 04 15:29:44 2007 +0100
    15.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/lookup.ML	Thu Jan 04 17:11:09 2007 +0100
    15.3 @@ -5,8 +5,7 @@
    15.4  struct
    15.5  
    15.6  fun lookup ((k, v) :: xs) l =
    15.7 -  (if ((k : string) = l) then SOME v else lookup xs l)
    15.8 -  | lookup [] l = NONE;
    15.9 +  (if ((k : string) = l) then SOME v else lookup xs l);
   15.10  
   15.11  end; (*struct Codegen*)
   15.12  
    16.1 --- a/doc-src/IsarAdvanced/Codegen/Thy/examples/pick1.ML	Thu Jan 04 15:29:44 2007 +0100
    16.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/pick1.ML	Thu Jan 04 17:11:09 2007 +0100
    16.3 @@ -6,13 +6,9 @@
    16.4  
    16.5  datatype nat = Zero_nat | Suc of nat;
    16.6  
    16.7 -fun less_nat Zero_nat (Suc n) = true
    16.8 -  | less_nat n Zero_nat = false
    16.9 -  | less_nat (Suc m) (Suc n) = less_nat m n;
   16.10 +fun less_nat Zero_nat (Suc n) = true;
   16.11  
   16.12 -fun minus_nat (Suc m) (Suc n) = minus_nat m n
   16.13 -  | minus_nat Zero_nat n = Zero_nat
   16.14 -  | minus_nat y Zero_nat = y;
   16.15 +fun minus_nat (Suc m) (Suc n) = minus_nat m n;
   16.16  
   16.17  end; (*struct Nat*)
   16.18  
   16.19 @@ -20,13 +16,7 @@
   16.20  struct
   16.21  
   16.22  fun pick ((k, v) :: xs) n =
   16.23 -  (if Nat.less_nat n k then v else pick xs (Nat.minus_nat n k))
   16.24 -  | pick (x :: xs) n =
   16.25 -    let
   16.26 -      val (ka, va) = x;
   16.27 -    in
   16.28 -      (if Nat.less_nat n ka then va else pick xs (Nat.minus_nat n ka))
   16.29 -    end;
   16.30 +  (if Nat.less_nat n k then v else pick xs (Nat.minus_nat n k));
   16.31  
   16.32  end; (*struct Codegen*)
   16.33  
    17.1 --- a/doc-src/IsarAdvanced/Codegen/Thy/examples/pick2.ML	Thu Jan 04 15:29:44 2007 +0100
    17.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/pick2.ML	Thu Jan 04 17:11:09 2007 +0100
    17.3 @@ -6,13 +6,9 @@
    17.4  
    17.5  datatype nat = Zero_nat | Suc of nat;
    17.6  
    17.7 -fun less_nat Zero_nat (Suc n) = true
    17.8 -  | less_nat n Zero_nat = false
    17.9 -  | less_nat (Suc m) (Suc n) = less_nat m n;
   17.10 +fun less_nat Zero_nat (Suc n) = true;
   17.11  
   17.12 -fun minus_nat (Suc m) (Suc n) = minus_nat m n
   17.13 -  | minus_nat Zero_nat n = Zero_nat
   17.14 -  | minus_nat y Zero_nat = y;
   17.15 +fun minus_nat (Suc m) (Suc n) = minus_nat m n;
   17.16  
   17.17  end; (*struct Nat*)
   17.18