--- a/Quot/Examples/FSet.thy	Tue Dec 08 22:05:01 2009 +0100
+++ b/Quot/Examples/FSet.thy	Tue Dec 08 23:04:25 2009 +0100
@@ -444,6 +444,15 @@
 (* apply (tactic {* procedure_tac @{context} @{thm ttt3} 1 *}) *)
 sorry
 
+(* Always safe to apply, but not too helpful *)
+lemma app_prs2:
+  assumes q1: "Quotient R1 abs1 rep1"
+  and     q2: "Quotient R2 abs2 rep2"
+  shows  "((abs1 ---> rep2) ((rep1 ---> abs2) f) (rep1 x)) = rep2 (((rep1 ---> abs2) f) x)"
+unfolding expand_fun_eq
+using Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2]
+by simp
+
 lemma hard: "(\<lambda>P. \<lambda>Q. P (Q (x::'a list))) = (\<lambda>P. \<lambda>Q. Q (P (x::'a list)))"
 sorry
 
@@ -452,14 +461,26 @@
 defer
 apply(injection)
 apply(subst babs_prs)
-defer defer
+apply(tactic {* quotient_tac @{context} 1 *})
+apply(tactic {* quotient_tac @{context} 1 *})
 apply(subst babs_prs)
-defer defer
+apply(tactic {* quotient_tac @{context} 1 *})
+apply(tactic {* quotient_tac @{context} 1 *})
 apply(subst babs_prs)
-defer defer
+apply(tactic {* quotient_tac @{context} 1 *})
+apply(tactic {* quotient_tac @{context} 1 *})
 apply(subst babs_prs)
-defer defer
+apply(tactic {* quotient_tac @{context} 1 *})
+apply(tactic {* quotient_tac @{context} 1 *})
+apply(subst all_prs)
+apply(tactic {* quotient_tac @{context} 1 *})
+apply(tactic {* lambda_prs_tac @{context} 1 *})
+apply(subst fun_map.simps)
 apply(tactic {* lambda_prs_tac @{context} 1 *})
-(* Until here is ok *)
+apply(subst fun_map.simps)
+apply(subst fun_map.simps)
+apply(tactic {* lambda_prs_tac @{context} 1 *})
 apply(cleaning)
+sorry
+
 end