equal
deleted
inserted
replaced
26 |
26 |
27 consts |
27 consts |
28 iSuc :: "inat => inat" |
28 iSuc :: "inat => inat" |
29 |
29 |
30 syntax (xsymbols) |
30 syntax (xsymbols) |
|
31 Infty :: inat ("\<infinity>") |
|
32 |
|
33 syntax (HTML output) |
31 Infty :: inat ("\<infinity>") |
34 Infty :: inat ("\<infinity>") |
32 |
35 |
33 defs |
36 defs |
34 Zero_inat_def: "0 == Fin 0" |
37 Zero_inat_def: "0 == Fin 0" |
35 iSuc_def: "iSuc i == case i of Fin n => Fin (Suc n) | \<infinity> => \<infinity>" |
38 iSuc_def: "iSuc i == case i of Fin n => Fin (Suc n) | \<infinity> => \<infinity>" |