--- a/Quot/Examples/FSet3.thy	Sat Dec 12 05:12:50 2009 +0100
+++ b/Quot/Examples/FSet3.thy	Sat Dec 12 09:27:06 2009 +0100
@@ -34,11 +34,11 @@
 
 
 lemma no_mem_nil: 
-  "(\<forall>a. \<not>(a \<in> set A)) = (A = [])"
+  "(\<forall>a. a \<notin> set A) = (A = [])"
 by (induct A) (auto)
 
 lemma none_mem_nil: 
-  "(\<forall>a. \<not>(a \<in> set A)) = (A \<approx> [])"
+  "(\<forall>a. a \<notin> set A) = (A \<approx> [])"
 by simp
 
 lemma mem_cons: 
@@ -235,7 +235,7 @@
   as "delete_raw"
 
 quotient_def
-  "funion :: 'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset" ("_ \<in>f _" [50, 51] 50)
+  "funion :: 'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset" ("_ \<union>f _" [50, 51] 50)
   as "op @"
 
 quotient_def
@@ -267,6 +267,8 @@
   MEM x [] = F
   MEM x (h::t) = (x=h) \/ MEM x t *)
 thm none_mem_nil
+(*lemma "(\<forall>a. a \<notin>f A) = (A = fempty)"*)
+
 thm mem_cons
 thm finite_set_raw_strong_cases
 thm card_raw.simps