equal
deleted
inserted
replaced
22 |
22 |
23 notation (HTML output) |
23 notation (HTML output) |
24 Infty ("\<infinity>") |
24 Infty ("\<infinity>") |
25 |
25 |
26 |
26 |
27 lemma not_Infty_eq[simp]: "(x ~= Infty) = (EX i. x = Fin i)" |
27 lemma not_Infty_eq[iff]: "(x ~= Infty) = (EX i. x = Fin i)" |
|
28 by (cases x) auto |
|
29 |
|
30 lemma not_Fin_eq [iff]: "(ALL y. x ~= Fin y) = (x = Infty)" |
28 by (cases x) auto |
31 by (cases x) auto |
29 |
32 |
30 |
33 |
31 subsection {* Constructors and numbers *} |
34 subsection {* Constructors and numbers *} |
32 |
35 |