equal
deleted
inserted
replaced
62 |
62 |
63 defs |
63 defs |
64 Zero_def "0 == Abs_Nat(Zero_Rep)" |
64 Zero_def "0 == Abs_Nat(Zero_Rep)" |
65 Suc_def "Suc == (%n. Abs_Nat(Suc_Rep(Rep_Nat(n))))" |
65 Suc_def "Suc == (%n. Abs_Nat(Suc_Rep(Rep_Nat(n))))" |
66 |
66 |
67 (*nat operations and recursion*) |
67 (*nat operations*) |
68 pred_nat_def "pred_nat == {(m,n). n = Suc m}" |
68 pred_nat_def "pred_nat == {(m,n). n = Suc m}" |
69 |
69 |
70 less_def "m<n == (m,n):trancl(pred_nat)" |
70 less_def "m<n == (m,n):trancl(pred_nat)" |
71 |
71 |
72 le_def "m<=(n::nat) == ~(n<m)" |
72 le_def "m<=(n::nat) == ~(n<m)" |