changeset 24421 | acfb2413faa3 |
parent 23850 | f1434532a562 |
child 26318 | 967323f93c67 |
24420:9fa337721689 | 24421:acfb2413faa3 |
---|---|
1 structure Nat = |
1 structure Nat = |
2 struct |
2 struct |
3 |
3 |
4 datatype nat = Zero_nat | Suc of nat; |
4 datatype nat = Suc of nat | Zero_nat; |
5 |
5 |
6 fun less_nat n (Suc m) = less_eq_nat n m |
6 fun less_nat n (Suc m) = less_eq_nat n m |
7 | less_nat n Zero_nat = false |
7 | less_nat n Zero_nat = false |
8 and less_eq_nat (Suc n) m = less_nat n m |
8 and less_eq_nat (Suc n) m = less_nat n m |
9 | less_eq_nat Zero_nat m = true; |
9 | less_eq_nat Zero_nat m = true; |