--- a/Nominal/Abs.thy	Sat Aug 28 13:41:31 2010 +0800
+++ b/Nominal/Abs.thy	Sat Aug 28 18:15:23 2010 +0800
@@ -568,16 +568,6 @@
   and   "Abs_res bs x = Abs_res cs y \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>res (op =) supp p (cs, y))"
   and   "Abs_lst bsl x = Abs_lst csl y \<longleftrightarrow> (\<exists>p. (bsl, x) \<approx>lst (op =) supp p (csl, y))"
   by (lifting alphas_abs)
-
-lemma split_rsp2[quot_respect]: "((R1 ===> R2 ===> prod_rel R1 R2 ===> op =) ===>
-  prod_rel R1 R2 ===> prod_rel R1 R2 ===> op =) split split"
-  by auto
-
-lemma split_prs2[quot_preserve]:
-  assumes q1: "Quotient R1 Abs1 Rep1"
-  and q2: "Quotient R2 Abs2 Rep2"
-  shows "((Abs1 ---> Abs2 ---> prod_fun Abs1 Abs2 ---> id) ---> prod_fun Rep1 Rep2 ---> prod_fun Rep1 Rep2 ---> id) split = split"
-  by (simp add: expand_fun_eq Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2])
 *)
 
 

--- a/Nominal/Nominal2_FSet.thy	Sat Aug 28 13:41:31 2010 +0800
+++ b/Nominal/Nominal2_FSet.thy	Sat Aug 28 18:15:23 2010 +0800
@@ -5,20 +5,16 @@
         FSet 
 begin
 
-lemma "p \<bullet> {} = {}"
-apply(perm_simp)
-by simp
-
 lemma permute_rsp_fset[quot_respect]:
-  "(op = ===> list_eq ===> list_eq) permute permute"
-  apply (simp add: eqvts[symmetric])
-  apply clarify
-  apply (subst permute_minus_cancel(1)[symmetric, of "xb"])
-  apply (subst mem_eqvt[symmetric])
-  apply (subst (2) permute_minus_cancel(1)[symmetric, of "xb"])
-  apply (subst mem_eqvt[symmetric])
-  apply (erule_tac x="- x \<bullet> xb" in allE)
-  apply simp
+  shows "(op = ===> list_eq ===> list_eq) permute permute"
+  apply(simp)
+  apply(clarify)
+  apply(simp add: eqvts[symmetric])  
+  apply(subst permute_minus_cancel(1)[symmetric, of "xb"])
+  apply(subst mem_eqvt[symmetric])
+  apply(subst (2) permute_minus_cancel(1)[symmetric, of "xb"])
+  apply(subst mem_eqvt[symmetric])
+  apply(simp)
   done
 
 instantiation fset :: (pt) pt
@@ -40,29 +36,14 @@
 
 end
 
-lemma "p \<bullet> {} = {}"
-apply(perm_simp)
-by simp
-
 lemma permute_fset[simp]:
   fixes S::"('a::pt) fset"
   shows "(p \<bullet> {||}) = ({||} ::('a::pt) fset)"
   and "p \<bullet> finsert x S = finsert (p \<bullet> x) (p \<bullet> S)"
   by (lifting permute_list.simps)
 
-lemma "p \<bullet> {} = {}"
-apply(perm_simp)
-by simp
-
-ML {* @{term "{}"} ; @{term "{||}"} *}
-
 declare permute_fset[eqvt]
 
-lemma "p \<bullet> {} = {}"
-apply(perm_simp)
-by simp
-
-
 lemma fmap_eqvt[eqvt]: 
   shows "p \<bullet> (fmap f S) = fmap (p \<bullet> f) (p \<bullet> S)"
   by (lifting map_eqvt)
@@ -80,6 +61,11 @@
   unfolding supp_def
   by (perm_simp) (simp add: fset_cong)
 
+lemma supp_fempty:
+  shows "supp {||} = {}"
+  unfolding supp_def
+  by simp
+
 lemma supp_finsert:
   fixes x::"'a::fs"
   shows "supp (finsert x S) = supp x \<union> supp S"
@@ -89,10 +75,6 @@
   apply(simp add: supp_fset_to_set)
   done
 
-lemma supp_fempty:
-  shows "supp {||} = {}"
-  unfolding supp_def
-  by simp
 
 instance fset :: (fs) fs
   apply (default)
@@ -125,8 +107,9 @@
   done
 
 lemma fresh_star_atom:
-  "fset_to_set s \<sharp>* (a :: _ :: at_base) \<Longrightarrow> atom a \<sharp> fset_to_set s"
-  apply (induct s)
+  fixes a::"'a::at_base"
+  shows "fset_to_set S \<sharp>* a \<Longrightarrow> atom a \<sharp> fset_to_set S"
+  apply (induct S)
   apply (simp add: fresh_set_empty)
   apply simp
   apply (unfold fresh_def)
@@ -140,8 +123,4 @@
   apply auto
   done
 
-lemma "p \<bullet> {} = {}"
-apply(perm_simp)
-by simp
-
 end