equal
deleted
inserted
replaced
1 structure HOL = |
1 structure HOL = |
2 struct |
2 struct |
3 |
3 |
4 datatype boola = True | False; |
4 datatype boola = False | True; |
5 |
5 |
6 fun anda x True = x |
6 fun anda x True = x |
7 | anda x False = False |
7 | anda x False = False |
8 | anda True x = x |
8 | anda True x = x |
9 | anda False x = False; |
9 | anda False x = False; |
11 end; (*struct HOL*) |
11 end; (*struct HOL*) |
12 |
12 |
13 structure Nat = |
13 structure Nat = |
14 struct |
14 struct |
15 |
15 |
16 datatype nat = Zero_nat | Suc of nat; |
16 datatype nat = Suc of nat | Zero_nat; |
17 |
17 |
18 fun less_nat n (Suc m) = less_eq_nat n m |
18 fun less_nat n (Suc m) = less_eq_nat n m |
19 | less_nat n Zero_nat = HOL.False |
19 | less_nat n Zero_nat = HOL.False |
20 and less_eq_nat (Suc n) m = less_nat n m |
20 and less_eq_nat (Suc n) m = less_nat n m |
21 | less_eq_nat Zero_nat m = HOL.True; |
21 | less_eq_nat Zero_nat m = HOL.True; |