--- a/Nominal/FSet.thy	Wed Apr 14 07:57:55 2010 +0200
+++ b/Nominal/FSet.thy	Wed Apr 14 08:16:54 2010 +0200
@@ -1,3 +1,9 @@
+(*  Title:      Quotient.thy
+    Author:     Cezary Kaliszyk 
+    Author:     Christian Urban
+
+    provides a reasoning infrastructure for the type of finite sets
+*)
 theory FSet
 imports Quotient Quotient_List List
 begin
@@ -9,7 +15,8 @@
 
 lemma list_eq_equivp:
   shows "equivp list_eq"
-unfolding equivp_reflp_symp_transp reflp_def symp_def transp_def
+unfolding equivp_reflp_symp_transp 
+unfolding reflp_def symp_def transp_def
 by auto
 
 quotient_type
@@ -48,7 +55,7 @@
 abbreviation
   fnotin :: "'a \<Rightarrow> 'a fset \<Rightarrow> bool" ("_ |\<notin>| _" [50, 51] 50)
 where
-  "a |\<notin>| S \<equiv> \<not>(a |\<in>| S)"
+  "x |\<notin>| S \<equiv> \<not>(x |\<in>| S)"
 
 lemma memb_rsp[quot_respect]:
   shows "(op = ===> op \<approx> ===> op =) memb memb"
@@ -66,12 +73,12 @@
 
 lemma nil_not_cons:
   shows
-  "\<not>[] \<approx> x # xs"
-  "\<not>x # xs \<approx> []"
+  "\<not> ([] \<approx> x # xs)"
+  "\<not> (x # xs \<approx> [])"
   by auto
 
 lemma not_memb_nil:
-  "\<not>memb x []"
+  "\<not> memb x []"
   by (simp add: memb_def)
 
 lemma memb_cons_iff:
@@ -131,7 +138,7 @@
 
 lemma fcard_raw_not_memb:
   fixes x :: "'a"
-  shows "\<not>(memb x xs) \<longleftrightarrow> (fcard_raw (x # xs) = Suc (fcard_raw xs))"
+  shows "\<not>(memb x xs) \<longleftrightarrow> fcard_raw (x # xs) = Suc (fcard_raw xs)"
   by auto
 
 lemma fcard_raw_suc:
@@ -178,10 +185,8 @@
 
 lemma fcard_raw_1:
   fixes a :: "'a list"
-  shows "(fcard_raw xs = 1) = (\<exists>x. xs \<approx> [x])"
-  apply auto
-  apply (drule fcard_raw_suc)
-  apply clarify
+  shows "fcard_raw xs = 1 \<longleftrightarrow> (\<exists>x. xs \<approx> [x])"
+  apply (auto dest!: fcard_raw_suc)
   apply (simp add: fcard_raw_0)
   apply (rule_tac x="x" in exI)
   apply simp
@@ -223,7 +228,7 @@
   by simp
 
 lemma memb_append:
-  "memb x (xs @ ys) = (memb x xs \<or> memb x ys)"
+  "memb x (xs @ ys) \<longleftrightarrow> memb x xs \<or> memb x ys"
   by (induct xs) (simp_all add: not_memb_nil memb_cons_iff)
 
 text {* raw section *}
@@ -375,7 +380,7 @@
   by (induct l) (simp_all add: not_memb_nil)
 
 lemma memb_finter_raw:
-  "memb x (finter_raw xs ys) = (memb x xs \<and> memb x ys)"
+  "memb x (finter_raw xs ys) \<longleftrightarrow> memb x xs \<and> memb x ys"
   apply (induct xs)
   apply (simp add: not_memb_nil)
   apply (simp add: finter_raw.simps)