equal
deleted
inserted
replaced
91 end |
91 end |
92 |
92 |
93 interpretation nat_int: type_definition [int nat "Collect (op <= 0)"] |
93 interpretation nat_int: type_definition [int nat "Collect (op <= 0)"] |
94 by (rule td_nat_int) |
94 by (rule td_nat_int) |
95 |
95 |
96 -- "resetting to the default nat induct and cases rules" |
96 text "resetting to the default nat induct and cases rules" |
97 declare Nat.induct [case_names 0 Suc, induct type] |
97 declare nat_induct [induct type: nat] |
98 declare Nat.exhaust [case_names 0 Suc, cases type] |
98 declare nat.exhaust [cases type: nat] |
99 |
99 |
100 |
100 |
101 subsection "Extended form of type definition predicate" |
101 subsection "Extended form of type definition predicate" |
102 |
102 |
103 lemma td_conds: |
103 lemma td_conds: |