--- a/src/HOL/Hyperreal/StarDef.thy Wed May 07 10:56:58 2008 +0200
+++ b/src/HOL/Hyperreal/StarDef.thy Wed May 07 10:57:19 2008 +0200
@@ -18,7 +18,7 @@
lemma freeultrafilter_FreeUltrafilterNat: "freeultrafilter \<U>"
apply (unfold FreeUltrafilterNat_def)
-apply (rule someI_ex)
+apply (rule someI_ex [where P=freeultrafilter])
apply (rule freeultrafilter_Ex)
apply (rule nat_infinite)
done
@@ -401,10 +401,10 @@
by (transfer Int_def, rule refl)
lemma starset_Compl: "*s* -A = -( *s* A)"
-by (transfer Compl_def, rule refl)
+by (transfer Compl_eq, rule refl)
lemma starset_diff: "*s* (A - B) = *s* A - *s* B"
-by (transfer set_diff_def, rule refl)
+by (transfer set_diff_eq, rule refl)
lemma starset_image: "*s* (f ` A) = ( *f* f) ` ( *s* A)"
by (transfer image_def, rule refl)
@@ -413,7 +413,7 @@
by (transfer vimage_def, rule refl)
lemma starset_subset: "( *s* A \<subseteq> *s* B) = (A \<subseteq> B)"
-by (transfer subset_def, rule refl)
+by (transfer subset_eq, rule refl)
lemma starset_eq: "( *s* A = *s* B) = (A = B)"
by (transfer, rule refl)