equal
deleted
inserted
replaced
53 local |
53 local |
54 |
54 |
55 instantiation nat :: zero |
55 instantiation nat :: zero |
56 begin |
56 begin |
57 |
57 |
58 definition Zero_nat_def [code func del]: |
58 definition Zero_nat_def [code del]: |
59 "0 = Abs_Nat Zero_Rep" |
59 "0 = Abs_Nat Zero_Rep" |
60 |
60 |
61 instance .. |
61 instance .. |
62 |
62 |
63 end |
63 end |
1279 context semiring_1 |
1279 context semiring_1 |
1280 begin |
1280 begin |
1281 |
1281 |
1282 definition |
1282 definition |
1283 Nats :: "'a set" where |
1283 Nats :: "'a set" where |
1284 [code func del]: "Nats = range of_nat" |
1284 [code del]: "Nats = range of_nat" |
1285 |
1285 |
1286 notation (xsymbols) |
1286 notation (xsymbols) |
1287 Nats ("\<nat>") |
1287 Nats ("\<nat>") |
1288 |
1288 |
1289 lemma of_nat_in_Nats [simp]: "of_nat n \<in> \<nat>" |
1289 lemma of_nat_in_Nats [simp]: "of_nat n \<in> \<nat>" |