diff -r 5ededdde9e9f -r c86a47d4966e Quot/Examples/FSet.thy
--- a/Quot/Examples/FSet.thy	Wed Dec 09 00:54:46 2009 +0100
+++ b/Quot/Examples/FSet.thy	Wed Dec 09 05:59:49 2009 +0100
@@ -384,9 +384,6 @@
 apply(simp)
 apply(rule allI)
 apply(rule list_eq_refl)
-apply(cleaning)
-apply(simp add: fun_map.simps expand_fun_eq)
-apply(cleaning)
 done
 
 lemma ttt3: "(\<lambda>x. ((op @) x ((op #) e []))) = (\<lambda>x. ((op #) e x))"
@@ -396,24 +393,12 @@
 (* 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
 
 (* PROBLEM *)
 lemma hard_lift: "(\<lambda>P. \<lambda>Q. P (Q (x::'a fset))) = (\<lambda>P. \<lambda>Q. Q (P (x::'a fset)))"
-apply(lifting_setup hard)
-defer
-apply(injection)
-apply(cleaning)
+apply(lifting hard)
 sorry
 
 end