changeset 17429 | e8d6ed3aacfe |
parent 17318 | bc1c75855f3d |
child 17431 | 70311ad8bf11 |
--- a/src/HOL/Hyperreal/NSA.thy Thu Sep 15 23:16:04 2005 +0200 +++ b/src/HOL/Hyperreal/NSA.thy Thu Sep 15 23:46:22 2005 +0200 @@ -1777,7 +1777,7 @@ lemma FreeUltrafilterNat_Rep_hypreal: "[| X \<in> Rep_star x; Y \<in> Rep_star x |] ==> {n. X n = Y n} \<in> FreeUltrafilterNat" -by (rule_tac z = x in eq_Abs_star, auto, ultra) +by (cases x, unfold star_n_def, auto, ultra) lemma HFinite_FreeUltrafilterNat: "x \<in> HFinite