| changeset 25382 | 72cfe89f7b21 |
| parent 25231 | 1aa9c8f022d0 |
| child 25482 | 4ed49eccb1eb |
| 25381:c100bf5bd6b8 | 25382:72cfe89f7b21 |
|---|---|
1442 |
1442 |
1443 context semiring_1 |
1443 context semiring_1 |
1444 begin |
1444 begin |
1445 |
1445 |
1446 definition |
1446 definition |
1447 Nats :: "'a set" |
1447 Nats :: "'a set" where |
1448 where |
|
1449 "Nats = range of_nat" |
1448 "Nats = range of_nat" |
1450 |
|
1451 end |
|
1452 |
1449 |
1453 notation (xsymbols) |
1450 notation (xsymbols) |
1454 Nats ("\<nat>") |
1451 Nats ("\<nat>") |
1452 |
|
1453 end |
|
1455 |
1454 |
1456 context semiring_1 |
1455 context semiring_1 |
1457 begin |
1456 begin |
1458 |
1457 |
1459 lemma of_nat_in_Nats [simp]: "of_nat n \<in> \<nat>" |
1458 lemma of_nat_in_Nats [simp]: "of_nat n \<in> \<nat>" |