--- a/Nominal/FSet.thy	Tue Jul 20 06:14:16 2010 +0100
+++ b/Nominal/FSet.thy	Thu Jul 22 08:30:50 2010 +0200
@@ -107,23 +107,6 @@
   unfolding list_eq.simps
   by (simp only: set_map set_in_eq)
 
-text {* Peter *}
-ML {* Quotient_Info.quotient_rules_get @{context} *}
-
-lemma 
-  assumes "Quotient R1 abs1 rep1"
-  and     "Quotient R2 abs2 rep2"
-  shows   "Quotient (R1 OOO R2) (abs1 o ab2) (rep1 o rep2)"
-using assms
-sorry
-
-lemma 
-  assumes "Quotient R1 abs1 rep1"
-  and     "Quotient R2 abs2 rep2"
-  shows   "Quotient (R3) (abs1 o ab2) (rep1 o rep2)"
-using assms
-sorry
-
 lemma quotient_compose_list[quot_thm]:
   shows  "Quotient ((list_all2 op \<approx>) OOO (op \<approx>))
     (abs_fset \<circ> (map abs_fset)) ((map rep_fset) \<circ> rep_fset)"
@@ -740,7 +723,7 @@
 
 lemma singleton_list_eq:
   shows "[x] \<approx> [y] \<longleftrightarrow> x = y"
-  by (simp add: id_simps) auto
+  by (simp add:) auto
 
 lemma sub_list_cons:
   "sub_list (x # xs) ys = (memb x ys \<and> sub_list xs ys)"
@@ -764,7 +747,7 @@
   assumes a: "fcard_raw xs = Suc n"
   shows "\<exists>x ys. \<not> (memb x ys) \<and> xs \<approx> (x # ys) \<and> fcard_raw ys = n"
   using a
-  by (induct xs) (auto simp add: memb_def split: if_splits)
+  by (induct xs) (auto simp add: memb_def split_ifs)
 
 lemma singleton_fcard_1:
   shows "set xs = {x} \<Longrightarrow> fcard_raw xs = 1"
@@ -965,7 +948,7 @@
   by (auto simp add: sub_list_set)
 
 lemma fcard_raw_set: "fcard_raw xs = card (set xs)"
-  by (induct xs) (auto simp add: insert_absorb memb_def card_insert_disjoint finite_set)
+  by (induct xs) (auto simp add: insert_absorb memb_def card_insert_disjoint)
 
 lemma memb_set: "memb x xs = (x \<in> set xs)"
   by (simp only: memb_def)
@@ -982,7 +965,7 @@
 
 lemma fminus_raw_set: "set (fminus_raw xs ys) = set xs - set ys"
   by (induct ys arbitrary: xs)
-     (simp_all add: fminus_raw.simps delete_raw_set, blast)
+     (simp_all add: delete_raw_set, blast)
 
 text {* Raw theorems of ffilter *}
 
@@ -1323,25 +1306,10 @@
   shows "fconcat {||} = {||}"
   by (lifting concat.simps(1))
 
-text {* Peter *}
-lemma test: "equivp R ==> a = b --> R a b"
-by (simp add: equivp_def)
-
-lemma 
-  shows "fconcat {||} = {||}"
-apply(lifting_setup concat.simps(1))
-apply(rule test)
-apply(tactic {* resolve_tac (Quotient_Info.equiv_rules_get @{context}) 1 *})
-
-sorry
-
 lemma fconcat_insert:
   shows "fconcat (finsert x S) = x |\<union>| fconcat S"
   by (lifting concat.simps(2))
 
-lemma "fconcat (xs |\<union>| ys) = fconcat xs |\<union>| fconcat ys"
-  by (lifting concat_append)
-
 text {* ffilter *}
 
 lemma subseteq_filter: "ffilter P xs <= ffilter Q xs = (\<forall> x. x |\<in>| xs \<longrightarrow> P x \<longrightarrow> Q x)"
@@ -1350,7 +1318,8 @@
 lemma eq_ffilter: "(ffilter P xs = ffilter Q xs) = (\<forall>x. x |\<in>| xs \<longrightarrow> P x = Q x)"
 by (lifting list_eq_filter)
 
-lemma subset_ffilter: "(\<And>x. x |\<in>| xs \<Longrightarrow> P x \<Longrightarrow> Q x) \<Longrightarrow> (x |\<in>| xs & \<not> P x & Q x) \<Longrightarrow> ffilter P xs < ffilter Q xs"
+lemma subset_ffilter: 
+  "(\<And>x. x |\<in>| xs \<Longrightarrow> P x \<Longrightarrow> Q x) \<Longrightarrow> (x |\<in>| xs & \<not> P x & Q x) \<Longrightarrow> ffilter P xs < ffilter Q xs"
 unfolding less_fset by (auto simp add: subseteq_filter eq_ffilter)
 
 section {* lemmas transferred from Finite_Set theory *}
@@ -1449,7 +1418,7 @@
 lemma list_all2_refl:
   assumes q: "equivp R"
   shows "(list_all2 R) r r"
-  by (rule list_all2_refl) (metis equivp_def fset_equivp q)
+  by (rule list_all2_refl) (metis equivp_def q)
 
 lemma compose_list_refl2:
   assumes q: "equivp R"