--- a/Nominal-General/Nominal2_Supp.thy	Sun Jul 18 19:07:05 2010 +0100
+++ b/Nominal-General/Nominal2_Supp.thy	Mon Jul 19 07:49:10 2010 +0100
@@ -193,7 +193,7 @@
       assume "a \<noteq> b"
       hence "atom a \<sharp> b" by (simp add: fresh_at_base)
       with a3 have "atom a \<sharp> h b" 
-	by (rule fresh_fun_app)
+        by (rule fresh_fun_app)
       with a2 have d1: "(atom b \<rightleftharpoons> atom a) \<bullet> (h b) = (h b)"
         by (rule swap_fresh_fresh)
       from a1 a3 have d2: "(atom b \<rightleftharpoons> atom a) \<bullet> h = h"
@@ -392,8 +392,8 @@
     moreover
     { assume "supp p \<noteq> {}"
       then obtain a where a0: "a \<in> supp p" by blast
-      then have a1: "p \<bullet> a \<in> S" "a \<in> S" "sort_of (p \<bullet> a) = sort_of a" "p \<bullet> a \<noteq> a" using as
-	by (auto simp add: supp_atom supp_perm swap_atom)
+      then have a1: "p \<bullet> a \<in> S" "a \<in> S" "sort_of (p \<bullet> a) = sort_of a" "p \<bullet> a \<noteq> a"
+        using as by (auto simp add: supp_atom supp_perm swap_atom)
       let ?q = "(p \<bullet> a \<rightleftharpoons> a) + p"
       have a2: "supp ?q \<subseteq> supp p" unfolding supp_perm by (auto simp add: swap_atom)
       moreover
@@ -503,14 +503,12 @@
   shows "(\<Union>x\<in>S. supp x) \<subseteq> supp S"
 proof -
   have "(\<Union>x\<in>S. supp x) = supp (\<Union>x\<in>S. supp x)"
-    apply(rule supp_finite_atom_set[symmetric])
-    apply(rule Union_of_fin_supp_sets[OF fin])
-    done
+    by (rule supp_finite_atom_set[symmetric])
+       (rule Union_of_fin_supp_sets[OF fin])
   also have "\<dots> \<subseteq> supp S"
-    apply(rule supp_subset_fresh)
-    apply(simp add: Union_fresh)
-    done
-  finally show ?thesis .
+    by (rule supp_subset_fresh)
+       (simp add: Union_fresh)
+  finally show "(\<Union>x\<in>S. supp x) \<subseteq> supp S" .
 qed
 
 lemma supp_of_fin_sets:

--- 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"