--- a/doc-src/IsarAdvanced/Codegen/Thy/examples/bool_infix.ML Fri Mar 02 15:43:16 2007 +0100
+++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/bool_infix.ML Fri Mar 02 15:43:17 2007 +0100
@@ -1,24 +1,15 @@
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
+fun less_nat n (Suc m) = less_eq_nat n m
| 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);
+and less_eq_nat (Suc n) m = less_nat n m
+ | less_eq_nat Zero_nat m = true;
end; (*struct Nat*)
--- a/doc-src/IsarAdvanced/Codegen/Thy/examples/bool_literal.ML Fri Mar 02 15:43:16 2007 +0100
+++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/bool_literal.ML Fri Mar 02 15:43:17 2007 +0100
@@ -6,9 +6,6 @@
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
@@ -21,11 +18,10 @@
datatype nat = Zero_nat | Suc of nat;
-fun less_nat Zero_nat (Suc n) = HOL.True
+fun less_nat n (Suc m) = less_eq_nat n m
| 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);
+and less_eq_nat (Suc n) m = less_nat n m
+ | less_eq_nat Zero_nat m = HOL.True;
end; (*struct Nat*)
--- a/doc-src/IsarAdvanced/Codegen/Thy/examples/bool_mlbool.ML Fri Mar 02 15:43:16 2007 +0100
+++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/bool_mlbool.ML Fri Mar 02 15:43:17 2007 +0100
@@ -1,24 +1,15 @@
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
+fun less_nat n (Suc m) = less_eq_nat n m
| 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);
+and less_eq_nat (Suc n) m = less_nat n m
+ | less_eq_nat Zero_nat m = true;
end; (*struct Nat*)
--- a/doc-src/IsarAdvanced/Codegen/Thy/examples/class.ML Fri Mar 02 15:43:16 2007 +0100
+++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/class.ML Fri Mar 02 15:43:17 2007 +0100
@@ -11,15 +11,15 @@
structure Codegen =
struct
-type 'a null = {Codegen__null : 'a};
-fun null (A_:'a null) = #Codegen__null A_;
+type 'a null = {null : 'a};
+fun null (A_:'a null) = #null A_;
fun head A_ (y :: xs) = y
| head A_ [] = null A_;
val null_option : 'a option = NONE;
-fun null_optiona () = {Codegen__null = null_option} : ('b option) null;
+fun null_optiona () = {null = null_option} : ('b option) null;
val dummy : Nat.nat option =
head (null_optiona ()) [SOME (Nat.Suc Nat.Zero_nat), NONE];
--- a/doc-src/IsarAdvanced/Codegen/Thy/examples/collect_duplicates.ML Fri Mar 02 15:43:16 2007 +0100
+++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/collect_duplicates.ML Fri Mar 02 15:43:17 2007 +0100
@@ -4,8 +4,8 @@
structure Code_Generator =
struct
-type 'a eq = {Code_Generator__op_eq : 'a -> 'a -> bool};
-fun op_eq (A_:'a eq) = #Code_Generator__op_eq A_;
+type 'a eq = {op_eq : 'a -> 'a -> bool};
+fun op_eq (A_:'a eq) = #op_eq A_;
end; (*struct Code_Generator*)
--- a/doc-src/IsarAdvanced/Codegen/Thy/examples/dirty_set.ML Fri Mar 02 15:43:16 2007 +0100
+++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/dirty_set.ML Fri Mar 02 15:43:17 2007 +0100
@@ -8,6 +8,17 @@
end; (*struct Nat*)
+structure Integer =
+struct
+
+fun nat_aux n i =
+ (if IntInf.<= (i, (0 : IntInf.int)) then n
+ else nat_aux (Nat.Suc n) (IntInf.- (i, (1 : IntInf.int))));
+
+fun nat i = nat_aux Nat.Zero_nat i;
+
+end; (*struct Integer*)
+
structure Codegen =
struct
@@ -15,7 +26,7 @@
val foobar_set : Nat.nat list =
Nat.Zero_nat ::
- (Nat.Suc Nat.Zero_nat :: (Nat.Suc (Nat.Suc Nat.Zero_nat) :: []));
+ (Nat.Suc Nat.Zero_nat :: (Integer.nat (2 : IntInf.int) :: []));
end; (*struct Codegen*)
--- a/doc-src/IsarAdvanced/Codegen/Thy/examples/lexicographic.ML Fri Mar 02 15:43:16 2007 +0100
+++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/lexicographic.ML Fri Mar 02 15:43:17 2007 +0100
@@ -4,19 +4,17 @@
structure Orderings =
struct
-type 'a ord =
- {Orderings__less_eq : 'a -> 'a -> bool,
- Orderings__less : 'a -> 'a -> bool};
-fun less_eq (A_:'a ord) = #Orderings__less_eq A_;
-fun less (A_:'a ord) = #Orderings__less A_;
+type 'a ord = {less_eq : 'a -> 'a -> bool, less : 'a -> 'a -> bool};
+fun less_eq (A_:'a ord) = #less_eq A_;
+fun less (A_:'a ord) = #less A_;
end; (*struct Orderings*)
structure Code_Generator =
struct
-type 'a eq = {Code_Generator__op_eq : 'a -> 'a -> bool};
-fun op_eq (A_:'a eq) = #Code_Generator__op_eq A_;
+type 'a eq = {op_eq : 'a -> 'a -> bool};
+fun op_eq (A_:'a eq) = #op_eq A_;
end; (*struct Code_Generator*)
--- a/doc-src/IsarAdvanced/Codegen/Thy/examples/pick1.ML Fri Mar 02 15:43:16 2007 +0100
+++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/pick1.ML Fri Mar 02 15:43:17 2007 +0100
@@ -6,9 +6,10 @@
datatype nat = Zero_nat | Suc of nat;
-fun less_nat Zero_nat (Suc n) = true
+fun less_nat n (Suc m) = less_eq_nat n m
| less_nat n Zero_nat = false
- | less_nat (Suc m) (Suc n) = less_nat m n;
+and less_eq_nat (Suc n) m = less_nat n m
+ | less_eq_nat Zero_nat m = true;
fun minus_nat (Suc m) (Suc n) = minus_nat m n
| minus_nat Zero_nat n = Zero_nat
--- a/doc-src/IsarAdvanced/Codegen/Thy/examples/pick2.ML Fri Mar 02 15:43:16 2007 +0100
+++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/pick2.ML Fri Mar 02 15:43:17 2007 +0100
@@ -6,9 +6,10 @@
datatype nat = Zero_nat | Suc of nat;
-fun less_nat Zero_nat (Suc n) = true
+fun less_nat n (Suc m) = less_eq_nat n m
| less_nat n Zero_nat = false
- | less_nat (Suc m) (Suc n) = less_nat m n;
+and less_eq_nat (Suc n) m = less_nat n m
+ | less_eq_nat Zero_nat m = true;
fun minus_nat (Suc m) (Suc n) = minus_nat m n
| minus_nat Zero_nat n = Zero_nat