src/HOL/Hyperreal/HyperDef.thy
changeset 19931 fb32b43e7f80
parent 19765 dfe940911617
child 20245 54db3583354f
     1.1 --- a/src/HOL/Hyperreal/HyperDef.thy	Tue Jun 20 14:51:59 2006 +0200
     1.2 +++ b/src/HOL/Hyperreal/HyperDef.thy	Tue Jun 20 15:53:44 2006 +0200
     1.3 @@ -58,6 +58,9 @@
     1.4  by (rule FreeUltrafilterNat_mem [THEN freeultrafilter.finite])
     1.5  
     1.6  lemma FreeUltrafilterNat_not_finite: "x \<in> FreeUltrafilterNat ==> ~ finite x"
     1.7 +thm FreeUltrafilterNat_mem
     1.8 +thm freeultrafilter.infinite
     1.9 +thm FreeUltrafilterNat_mem [THEN freeultrafilter.infinite]
    1.10  by (rule FreeUltrafilterNat_mem [THEN freeultrafilter.infinite])
    1.11  
    1.12  lemma FreeUltrafilterNat_empty [simp]: "{} \<notin> FreeUltrafilterNat"