--- a/src/HOL/Hyperreal/Filter.thy Tue Jul 04 12:13:38 2006 +0200
+++ b/src/HOL/Hyperreal/Filter.thy Tue Jul 04 14:47:01 2006 +0200
@@ -68,10 +68,10 @@
lemma (in freeultrafilter) finite: "finite A \<Longrightarrow> A \<notin> F"
by (erule contrapos_pn, erule infinite)
-lemma (in freeultrafilter) filter: "filter F" by intro_locales
+lemma (in freeultrafilter) filter: "filter F" by unfold_locales
lemma (in freeultrafilter) ultrafilter: "ultrafilter F"
- by intro_locales
+ by unfold_locales
subsection {* Collect properties *}
@@ -387,7 +387,7 @@
qed
from fil ultra free have "freeultrafilter U"
by (rule freeultrafilter.intro [OF ultrafilter.intro])
- (* FIXME: intro_locales should use chained facts *)
+ (* FIXME: unfold_locales should use chained facts *)
thus ?thesis ..
qed