--- a/src/HOL/Hyperreal/Filter.thy Tue Jun 20 14:51:59 2006 +0200
+++ b/src/HOL/Hyperreal/Filter.thy Tue Jun 20 15:53:44 2006 +0200
@@ -68,10 +68,11 @@
lemma (in freeultrafilter) finite: "finite A \<Longrightarrow> A \<notin> F"
by (erule contrapos_pn, erule infinite)
-lemma (in freeultrafilter) filter: "filter F" .
+lemma (in freeultrafilter) filter: "filter F" by intro_locales
lemma (in freeultrafilter) ultrafilter: "ultrafilter F"
-by (rule ultrafilter.intro)
+ by intro_locales
+
subsection {* Collect properties *}
@@ -385,7 +386,8 @@
with U show "infinite A" by (rule mem_superfrechet_all_infinite)
qed
from fil ultra free have "freeultrafilter U"
- by (rule freeultrafilter.intro)
+ by (rule freeultrafilter.intro [OF ultrafilter.intro])
+ (* FIXME: intro_locales should use chained facts *)
thus ?thesis ..
qed