equal
deleted
inserted
replaced
66 less_def "m<n == (m,n):trancl(pred_nat)" |
66 less_def "m<n == (m,n):trancl(pred_nat)" |
67 |
67 |
68 le_def "m<=(n::nat) == ~(n<m)" |
68 le_def "m<=(n::nat) == ~(n<m)" |
69 |
69 |
70 nat_rec_def "nat_rec n c d == |
70 nat_rec_def "nat_rec n c d == |
71 wfrec pred_nat (%f. nat_case c (%m. d m (f m))) n" |
71 wfrec pred_nat (%f. nat_case c (%m. d m (f m))) n" |
72 (*least number operator*) |
72 (*least number operator*) |
73 Least_def "Least(P) == @k. P(k) & (ALL j. j<k --> ~P(j))" |
73 Least_def "Least(P) == @k. P(k) & (ALL j. j<k --> ~P(j))" |
74 |
74 |
75 end |
75 end |