--- a/Nominal/FSet.thy	Sun Jul 18 19:07:05 2010 +0100
+++ b/Nominal/FSet.thy	Mon Jul 19 07:49:10 2010 +0100
@@ -26,7 +26,9 @@
   'a fset = "'a list" / "list_eq"
   by (rule list_eq_equivp)
 
-text {* Raw definitions *}
+text {* Raw definitions of membership, sublist, cardinality, 
+  intersection
+*}
 
 definition
   memb :: "'a \<Rightarrow> 'a list \<Rightarrow> bool"
@@ -42,20 +44,22 @@
   fcard_raw :: "'a list \<Rightarrow> nat"
 where
   fcard_raw_nil:  "fcard_raw [] = 0"
-| fcard_raw_cons: "fcard_raw (x # xs) = (if memb x xs then fcard_raw xs else Suc (fcard_raw xs))"
+| fcard_raw_cons: "fcard_raw (x # xs) = 
+    (if memb x xs then fcard_raw xs else Suc (fcard_raw xs))"
 
 primrec
   finter_raw :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
 where
   "finter_raw [] l = []"
 | "finter_raw (h # t) l =
-     (if memb h l then h # (finter_raw t l) else finter_raw t l)"
+    (if memb h l then h # (finter_raw t l) else finter_raw t l)"
 
 primrec
   delete_raw :: "'a list \<Rightarrow> 'a \<Rightarrow> 'a list"
 where
   "delete_raw [] x = []"
-| "delete_raw (a # xs) x = (if (a = x) then delete_raw xs x else a # (delete_raw xs x))"
+| "delete_raw (a # xs) x = 
+    (if (a = x) then delete_raw xs x else a # (delete_raw xs x))"
 
 primrec
   fminus_raw :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"