| changeset 31084 | f4db921165ce |
| parent 31077 | 28dd6fd3d184 |
| child 31094 | 7d6edb28bdbc |
--- a/src/HOL/Library/Nat_Infinity.thy Sat May 09 07:25:45 2009 +0200 +++ b/src/HOL/Library/Nat_Infinity.thy Sun May 10 14:21:41 2009 +0200 @@ -24,7 +24,10 @@ Infty ("\<infinity>") -lemma not_Infty_eq[simp]: "(x ~= Infty) = (EX i. x = Fin i)" +lemma not_Infty_eq[iff]: "(x ~= Infty) = (EX i. x = Fin i)" +by (cases x) auto + +lemma not_Fin_eq [iff]: "(ALL y. x ~= Fin y) = (x = Infty)" by (cases x) auto