--- a/doc-src/IsarAdvanced/Codegen/Thy/examples/bool1.ML Mon Nov 13 15:43:24 2006 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,40 +0,0 @@
-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*)
--- a/doc-src/IsarAdvanced/Codegen/Thy/examples/bool2.ML Mon Nov 13 15:43:24 2006 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,33 +0,0 @@
-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*)
--- a/doc-src/IsarAdvanced/Codegen/Thy/examples/bool3.ML Mon Nov 13 15:43:24 2006 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,32 +0,0 @@
-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*)