| changeset 17702 | ea88ddeafabe |
| parent 17589 | 58eeffd73be1 |
| child 18648 | 22f96cd085d5 |
| 17701:6928771d256e | 17702:ea88ddeafabe |
|---|---|
22 |
22 |
23 axioms |
23 axioms |
24 -- {* the axiom of infinity in 2 parts *} |
24 -- {* the axiom of infinity in 2 parts *} |
25 inj_Suc_Rep: "inj Suc_Rep" |
25 inj_Suc_Rep: "inj Suc_Rep" |
26 Suc_Rep_not_Zero_Rep: "Suc_Rep x \<noteq> Zero_Rep" |
26 Suc_Rep_not_Zero_Rep: "Suc_Rep x \<noteq> Zero_Rep" |
27 |
27 finalconsts |
28 Zero_Rep |
|
29 Suc_Rep |
|
28 |
30 |
29 subsection {* Type nat *} |
31 subsection {* Type nat *} |
30 |
32 |
31 text {* Type definition *} |
33 text {* Type definition *} |
32 |
34 |