--- a/Nominal/FSet.thy	Sat Jul 17 15:44:24 2010 +0100
+++ b/Nominal/FSet.thy	Sun Jul 18 16:06:34 2010 +0100
@@ -103,6 +103,22 @@
   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>))
@@ -164,7 +180,7 @@
 lemma append_rsp[quot_respect]:
   shows "(op \<approx> ===> op \<approx> ===> op \<approx>) op @ op @"
   apply(simp del: list_eq.simps)
-  by auto
+  by auto 
 
 lemma append_rsp_unfolded:
   "\<lbrakk>x \<approx> y; v \<approx> w\<rbrakk> \<Longrightarrow> x @ v \<approx> y @ w"
@@ -605,8 +621,6 @@
 is
   "concat"
 
-thm fconcat_def
-
 quotient_definition
   "ffilter :: ('a \<Rightarrow> bool) \<Rightarrow> 'a fset \<Rightarrow> 'a fset"
 is
@@ -1305,6 +1319,17 @@
   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))

--- a/Quotient-Paper/ROOT.ML	Sat Jul 17 15:44:24 2010 +0100
+++ b/Quotient-Paper/ROOT.ML	Sun Jul 18 16:06:34 2010 +0100
@@ -1,3 +1,4 @@
+quick_and_dirty := true;
 no_document use_thys ["Quotient", 
                       "LaTeXsugar",
                       "../Nominal/FSet" ];