# HG changeset patch
# User haftmann
# Date 1163429738 -3600
# Node ID 3844037a8e2d24a47b5c2af4e8200d1aace90bba
# Parent  51d9bf0b821f9ebcfbb91ec96cc7dc862d6dbd43
adjusted to new fun''

diff -r 51d9bf0b821f -r 3844037a8e2d doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy
--- a/doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy	Mon Nov 13 15:45:34 2006 +0100
+++ b/doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy	Mon Nov 13 15:55:38 2006 +0100
@@ -546,7 +546,6 @@
 fun
   in_interval :: "nat \<times> nat \<Rightarrow> nat \<Rightarrow> bool" where
   "in_interval (k, l) n \<longleftrightarrow> k \<le> n \<and> n \<le> l"
-termination by (auto_term "{}")
 (*<*)
 declare in_interval.simps [code func]
 (*>*)
@@ -718,7 +717,6 @@
       then collect_duplicates xs ys zs
       else collect_duplicates xs (z#ys) zs
     else collect_duplicates (z#xs) (z#ys) zs)"
-termination by (auto_term "measure (length o snd o snd)")
 (*<*)
 lemmas [code func] = collect_duplicates.simps
 (*>*)
@@ -809,7 +807,6 @@
   lookup :: "(key \<times> 'a) list \<Rightarrow> key \<Rightarrow> 'a option" where
   "lookup [] l = None"
   "lookup ((k, v) # xs) l = (if k = l then Some v else lookup xs l)"
-termination by (auto_term "measure (length o fst)")
 (*<*)
 lemmas [code func] = lookup.simps
 (*>*)
@@ -1115,7 +1112,6 @@
   dummy_option :: "'a list \<Rightarrow> 'a option" where
   "dummy_option (x#xs) = Some x"
   "dummy_option [] = arbitrary"
-termination by (auto_term "{}")
 (*<*)
 declare dummy_option.simps [code func]
 (*>*)
@@ -1184,7 +1180,7 @@
 
 text %mlref {*
   \begin{mldecls}
-  @{index_ML CodegenData.lazy: "(unit -> thm list) -> CodegenData.lthms"}
+  @{index_ML CodegenData.lazy: "(unit -> thm list) -> thm list Susp.T"}
   \end{mldecls}
 
   \begin{description}
@@ -1201,7 +1197,7 @@
   \begin{mldecls}
   @{index_ML CodegenData.add_func: "thm -> theory -> theory"} \\
   @{index_ML CodegenData.del_func: "thm -> theory -> theory"} \\
-  @{index_ML CodegenData.add_funcl: "CodegenConsts.const * CodegenData.lthms -> theory -> theory"} \\
+  @{index_ML CodegenData.add_funcl: "CodegenConsts.const * thm list Susp.T -> theory -> theory"} \\
   @{index_ML CodegenData.add_inline: "thm -> theory -> theory"} \\
   @{index_ML CodegenData.del_inline: "thm -> theory -> theory"} \\
   @{index_ML CodegenData.add_inline_proc: "(theory -> cterm list -> thm list)
@@ -1209,7 +1205,7 @@
   @{index_ML CodegenData.add_preproc: "(theory -> thm list -> thm list)
     -> theory -> theory"} \\
   @{index_ML CodegenData.add_datatype: "string * (((string * sort) list * (string * typ list) list)
-    * CodegenData.lthms) -> theory -> theory"} \\
+    * thm list Susp.T) -> theory -> theory"} \\
   @{index_ML CodegenData.del_datatype: "string -> theory -> theory"} \\
   @{index_ML CodegenData.get_datatype: "theory -> string
     -> ((string * sort) list * (string * typ list) list) option"} \\
diff -r 51d9bf0b821f -r 3844037a8e2d doc-src/IsarAdvanced/Codegen/Thy/examples/bool_infix.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/bool_infix.ML	Mon Nov 13 15:55:38 2006 +0100
@@ -0,0 +1,32 @@
+structure ROOT = 
+struct
+
+structure HOL = 
+struct
+
+fun nota false = true
+  | nota true = false;
+
+end; (*struct HOL*)
+
+structure Nat = 
+struct
+
+datatype nat = Zero_nat | Suc of nat;
+
+fun less_nat Zero_nat (Suc n) = true
+  | less_nat n Zero_nat = false
+  | less_nat (Suc m) (Suc n) = less_nat m n;
+
+fun less_eq_nat m n = HOL.nota (less_nat n m);
+
+end; (*struct Nat*)
+
+structure Codegen = 
+struct
+
+fun in_interval (k, l) n = Nat.less_eq_nat k n andalso Nat.less_eq_nat n l;
+
+end; (*struct Codegen*)
+
+end; (*struct ROOT*)
diff -r 51d9bf0b821f -r 3844037a8e2d doc-src/IsarAdvanced/Codegen/Thy/examples/bool_literal.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/bool_literal.ML	Mon Nov 13 15:55:38 2006 +0100
@@ -0,0 +1,40 @@
+structure ROOT = 
+struct
+
+structure HOL = 
+struct
+
+datatype boola = True | False;
+
+fun nota False = True
+  | nota True = False;
+
+fun op_conj y True = y
+  | op_conj x False = False
+  | op_conj True y = y
+  | op_conj False x = False;
+
+end; (*struct HOL*)
+
+structure Nat = 
+struct
+
+datatype nat = Zero_nat | Suc of nat;
+
+fun less_nat Zero_nat (Suc n) = HOL.True
+  | less_nat n Zero_nat = HOL.False
+  | less_nat (Suc m) (Suc n) = less_nat m n;
+
+fun less_eq_nat m n = HOL.nota (less_nat n m);
+
+end; (*struct Nat*)
+
+structure Codegen = 
+struct
+
+fun in_interval (k, l) n =
+  HOL.op_conj (Nat.less_eq_nat k n) (Nat.less_eq_nat n l);
+
+end; (*struct Codegen*)
+
+end; (*struct ROOT*)
diff -r 51d9bf0b821f -r 3844037a8e2d doc-src/IsarAdvanced/Codegen/Thy/examples/bool_mlbool.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/bool_mlbool.ML	Mon Nov 13 15:55:38 2006 +0100
@@ -0,0 +1,33 @@
+structure ROOT = 
+struct
+
+structure HOL = 
+struct
+
+fun nota false = true
+  | nota true = false;
+
+end; (*struct HOL*)
+
+structure Nat = 
+struct
+
+datatype nat = Zero_nat | Suc of nat;
+
+fun less_nat Zero_nat (Suc n) = true
+  | less_nat n Zero_nat = false
+  | less_nat (Suc m) (Suc n) = less_nat m n;
+
+fun less_eq_nat m n = HOL.nota (less_nat n m);
+
+end; (*struct Nat*)
+
+structure Codegen = 
+struct
+
+fun in_interval (k, l) n =
+  (Nat.less_eq_nat k n) andalso (Nat.less_eq_nat n l);
+
+end; (*struct Codegen*)
+
+end; (*struct ROOT*)