equal
deleted
inserted
replaced
9 fun nota False = True |
9 fun nota False = True |
10 | nota True = False; |
10 | nota True = False; |
11 |
11 |
12 fun op_conj y True = y |
12 fun op_conj y True = y |
13 | op_conj x False = False |
13 | op_conj x False = False |
14 | op_conj True ya = ya |
14 | op_conj True y = y |
15 | op_conj False xa = False; |
15 | op_conj False x = False; |
16 |
16 |
17 end; (*struct HOL*) |
17 end; (*struct HOL*) |
18 |
18 |
19 structure IntDef = |
19 structure IntDef = |
20 struct |
20 struct |
21 |
21 |
22 datatype nat = Zero_nat | Succ_nat of nat; |
22 datatype nat = Zero_nat | Succ_nat of nat; |
23 |
23 |
24 fun less_nat Zero_nat (Succ_nat n) = HOL.True |
24 fun less_nat Zero_nat (Succ_nat n) = HOL.True |
25 | less_nat na Zero_nat = HOL.False |
25 | less_nat n Zero_nat = HOL.False |
26 | less_nat (Succ_nat m) (Succ_nat nb) = less_nat m nb; |
26 | less_nat (Succ_nat m) (Succ_nat n) = less_nat m n; |
27 |
27 |
28 fun less_eq_nat m n = HOL.nota (less_nat n m); |
28 fun less_eq_nat m n = HOL.nota (less_nat n m); |
29 |
29 |
30 end; (*struct IntDef*) |
30 end; (*struct IntDef*) |
31 |
31 |