# HG changeset patch
# User haftmann
# Date 1163429134 -3600
# Node ID 51d9bf0b821f9ebcfbb91ec96cc7dc862d6dbd43
# Parent  b59f7cca0b0c2a8f492aaea01eb50e56eac22f8d
*** empty log message ***

diff -r b59f7cca0b0c -r 51d9bf0b821f doc-src/IsarAdvanced/Codegen/Thy/examples/bool1.ML
--- 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*)
diff -r b59f7cca0b0c -r 51d9bf0b821f doc-src/IsarAdvanced/Codegen/Thy/examples/bool2.ML
--- 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*)
diff -r b59f7cca0b0c -r 51d9bf0b821f doc-src/IsarAdvanced/Codegen/Thy/examples/bool3.ML
--- 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*)