# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1260290374 -3600
# Node ID 5cb44fe9ae8e4c2dbcf91d680c36c7365130cabe
# Parent  820c64273ce03b60ac2f20eab17257d17e9328dc# Parent  e472aa533a24d7ec172d429822c613498bc04286
merge

diff -r e472aa533a24 -r 5cb44fe9ae8e Quot/Examples/FSet.thy
--- a/Quot/Examples/FSet.thy	Tue Dec 08 17:34:10 2009 +0100
+++ b/Quot/Examples/FSet.thy	Tue Dec 08 17:39:34 2009 +0100
@@ -307,7 +307,10 @@
 by (tactic {* lift_tac @{context} @{thm m2} 1 *})
 
 lemma "INSERT a (INSERT a x) = INSERT a x"
-apply (tactic {* lift_tac @{context} @{thm list_eq.intros(4)} 1 *})
+apply (tactic {* procedure_tac @{context} @{thm list_eq.intros(4)} 1 *})
+apply (regularize)
+apply (injection)
+apply (cleaning)
 done
 
 lemma "x = xa \<Longrightarrow> INSERT a x = INSERT a xa"
@@ -340,9 +343,8 @@
 apply (tactic {* (ObjectLogic.full_atomize_tac THEN' gen_frees_tac @{context}) 1 *})
 apply(tactic {* procedure_tac @{context} @{thm list.induct} 1 *})
 apply(tactic {* regularize_tac @{context} 1 *})
-defer
+apply(injection)
 apply(tactic {* clean_tac @{context} 1 *})
-apply(tactic {* inj_repabs_tac @{context} 1*})+
 done
 
 lemma list_induct_part:
@@ -430,15 +432,14 @@
 sorry
 
 lemma "(\<lambda>e. (FUNION x (INSERT e EMPTY))) = (\<lambda>e. (INSERT e x))"
-apply (tactic {* procedure_tac @{context} @{thm ttt2} 1 *})
-apply(tactic {* regularize_tac @{context} 1 *})
+apply(lifting_setup ttt2)
+apply(regularize)
 apply(rule impI)
 apply(simp)
 apply(rule allI)
 apply(rule list_eq_refl)
-apply(tactic {* all_inj_repabs_tac @{context} 1*})
-apply(tactic {* clean_tac @{context} 1 *})
-apply(tactic {* clean_tac @{context} 1 *}) (* TODO: needs lambda_prs twice *)
+apply(injection)
+apply(tactic {* clean_tac @{context} 1 *}) (* This is an example that needs lambda_prs twice *)
 done
 
 lemma ttt3: "(\<lambda>x. ((op @) x ((op #) e []))) = (\<lambda>x. ((op #) e x))"
diff -r e472aa533a24 -r 5cb44fe9ae8e Quot/QuotMain.thy
--- a/Quot/QuotMain.thy	Tue Dec 08 17:34:10 2009 +0100
+++ b/Quot/QuotMain.thy	Tue Dec 08 17:39:34 2009 +0100
@@ -1056,8 +1056,7 @@
     val defs = map (Thm.varifyT o symmetric o #def) (qconsts_dest thy)
       (* FIXME: why is the Thm.varifyT needed: example where it fails is LamEx *)
     val thms1 = @{thms all_prs ex_prs} @ defs
-    val thms2 = @{thms eq_reflection[OF fun_map.simps]} @ (id_simps_get lthy)
-                @ @{thms Quotient_abs_rep Quotient_rel_rep} 
+    val thms2 = @{thms fun_map.simps Quotient_abs_rep Quotient_rel_rep} @ (id_simps_get lthy)
     fun simps thms = (mk_minimal_ss lthy) addsimps thms addSolver quotient_solver
   in
     EVERY' [lambda_prs_tac lthy,