| author | Walther Neuper <neuper@ist.tugraz.at> |
| Thu, 12 Aug 2010 15:03:34 +0200 | |
| branch | isac-from-Isabelle2009-2 |
| changeset 37913 | 20e3616b2d9c |
| parent 30209 | 2f4684e2ea95 |
| permissions | -rw-r--r-- |
1 structure HOL =
2 struct
4 datatype boola = False | True;
6 fun anda x True = x
7 | anda x False = False
8 | anda True x = x
9 | anda False x = False;
11 end; (*struct HOL*)
13 structure Nat =
14 struct
16 datatype nat = Suc of nat | Zero_nat;
18 fun less_nat m (Suc n) = less_eq_nat m n
19 | less_nat n Zero_nat = HOL.False
20 and less_eq_nat (Suc m) n = less_nat m n
21 | less_eq_nat Zero_nat n = HOL.True;
23 end; (*struct Nat*)
25 structure Codegen =
26 struct
28 fun in_interval (k, l) n =
29 HOL.anda (Nat.less_eq_nat k n) (Nat.less_eq_nat n l);
31 end; (*struct Codegen*)