diff -r c129354f2ff6 -r 3104d62e7a16 Quot/Examples/IntEx.thy
--- a/Quot/Examples/IntEx.thy	Wed Dec 16 14:28:48 2009 +0100
+++ b/Quot/Examples/IntEx.thy	Thu Dec 17 14:58:33 2009 +0100
@@ -135,13 +135,13 @@
 done
 
 lemma "PLUS a = PLUS a"
-apply(tactic {* procedure_tac @{context} @{thm test2} 1 *})
+apply(lifting_setup test2)
 apply(rule impI)
 apply(rule ballI)
 apply(rule apply_rsp[OF Quotient_my_int plus_rsp])
 apply(simp only: in_respects)
-apply(tactic {* all_inj_repabs_tac @{context} 1*})
-apply(tactic {* clean_tac @{context} 1 *})
+apply(injection)
+apply(cleaning)
 done
 
 lemma test3: "my_plus = my_plus"
@@ -149,7 +149,7 @@
 done
 
 lemma "PLUS = PLUS"
-apply(tactic {* procedure_tac @{context} @{thm test3} 1 *})
+apply(lifting_setup test3)
 apply(rule impI)
 apply(rule plus_rsp)
 apply(injection)
@@ -158,10 +158,7 @@
 
 
 lemma "PLUS a b = PLUS b a"
-apply(tactic {* procedure_tac @{context} @{thm plus_sym_pre} 1 *})
-apply(tactic {* regularize_tac @{context} 1 *})
-apply(tactic {* all_inj_repabs_tac @{context} 1*})
-apply(tactic {* clean_tac @{context} 1 *})
+apply(lifting plus_sym_pre)
 done
 
 lemma plus_assoc_pre:
@@ -173,10 +170,7 @@
   done
 
 lemma plus_assoc: "PLUS (PLUS x xa) xb = PLUS x (PLUS xa xb)"
-apply(tactic {* procedure_tac @{context} @{thm plus_assoc_pre} 1 *})
-apply(tactic {* regularize_tac @{context} 1 *})
-apply(tactic {* all_inj_repabs_tac @{context} 1*})
-apply(tactic {* clean_tac @{context} 1 *})
+apply(lifting plus_assoc_pre)
 done
 
 lemma int_induct_raw:
@@ -212,10 +206,7 @@
 sorry
 
 lemma "foldl PLUS x (h # t) = PLUS h (foldl PLUS x t)"
-apply(lifting_setup ho_tst2)
-apply(regularize)
-apply(injection)
-apply(cleaning)
+apply(lifting ho_tst2)
 done
 
 lemma ho_tst3: "foldl f (s::nat \<times> nat) ([]::(nat \<times> nat) list) = s"
@@ -236,46 +227,6 @@
 lemma lam_tst2: "(\<lambda>(y :: nat \<times> nat). y) = (\<lambda>(x :: nat \<times> nat). x)"
 by simp
 
-(* test about lifting identity equations *)
-
-ML {*
-(* helper code from QuotMain *)
-val pat_ball = @{term "Ball (Respects (R1 ===> R2)) P"}
-val pat_bex  = @{term "Bex (Respects (R1 ===> R2)) P"}
-val simproc = Simplifier.simproc_i @{theory} "" [pat_ball, pat_bex] (K (ball_bex_range_simproc))
-val simpset = (mk_minimal_ss @{context}) 
-                       addsimps @{thms ball_reg_eqv bex_reg_eqv babs_reg_eqv}
-                       addsimprocs [simproc] addSolver equiv_solver
-*}
-
-(* What regularising does *)
-(*========================*)
-
-(* 0. preliminary simplification step *)
-thm ball_reg_eqv bex_reg_eqv (* of no use: babs_reg_eqv *)
-    ball_reg_eqv_range bex_reg_eqv_range
-(* 1. first two rtacs *)
-thm ball_reg_right bex_reg_left
-(* 2. monos *)
-(* 3. commutation rules *)
-thm ball_all_comm bex_ex_comm
-(* 4. then rel-equality *)
-thm eq_imp_rel
-(* 5. then simplification like 0 *)
-(* finally jump to 1 *)
-
-
-(* What cleaning does *)
-(*====================*)
-
-(* 1. conversion *)
-thm lambda_prs
-(* 2. simplification with *)
-thm all_prs ex_prs
-(* 3. Simplification with *)
-thm fun_map.simps id_simps Quotient_abs_rep Quotient_rel_rep
-(* 4. Test for refl *)
-
 lemma
   shows "equivp (op \<approx>)"
   and "equivp ((op \<approx>) ===> (op \<approx>))"
@@ -295,11 +246,9 @@
 done
 
 lemma "(\<lambda>(y :: my_int). y) = (\<lambda>(x :: my_int). x)"
-apply(tactic {* procedure_tac @{context} @{thm lam_tst3a} 1 *})
+apply(lifting lam_tst3a)
 apply(rule impI)
 apply(rule lam_tst3a_reg)
-apply(tactic {* all_inj_repabs_tac @{context} 1*})
-apply(tactic {* clean_tac  @{context} 1 *})
 done
 
 lemma lam_tst3b: "(\<lambda>(y :: nat \<times> nat \<Rightarrow> nat \<times> nat). y) = (\<lambda>(x :: nat \<times> nat \<Rightarrow> nat \<times> nat). x)"