declare insert_iff [simp]

--- a/src/HOL/Hyperreal/Filter.thy	Thu Dec 14 21:46:59 2006 +0100
+++ b/src/HOL/Hyperreal/Filter.thy	Thu Dec 14 22:08:35 2006 +0100
@@ -71,7 +71,7 @@
 lemma (in freeultrafilter) singleton: "{x} \<notin> F"
 by (rule finite, simp)
 
-lemma (in freeultrafilter) insert_iff: "(insert x A \<in> F) = (A \<in> F)"
+lemma (in freeultrafilter) insert_iff [simp]: "(insert x A \<in> F) = (A \<in> F)"
 apply (subst insert_is_Un)
 apply (subst Un_iff)
 apply (simp add: singleton)