diff -r 2e51e1315839 -r 520a4084d064 Quot/Examples/IntEx.thy
--- a/Quot/Examples/IntEx.thy	Tue Dec 08 16:36:01 2009 +0100
+++ b/Quot/Examples/IntEx.thy	Tue Dec 08 17:30:00 2009 +0100
@@ -12,9 +12,9 @@
   apply(auto simp add: mem_def expand_fun_eq)
   done
 
-thm quotient_equiv
+thm quot_equiv
 
-thm quotient_thm
+thm quot_thm
 
 thm my_int_equivp
 
@@ -132,7 +132,7 @@
   apply(auto)
   done
 
-lemma plus_rsp[quotient_rsp]:
+lemma plus_rsp[quot_respect]:
   shows "(intrel ===> intrel ===> intrel) my_plus my_plus"
 by (simp)
 
@@ -171,8 +171,8 @@
 apply(tactic {* procedure_tac @{context} @{thm test3} 1 *})
 apply(rule impI)
 apply(rule plus_rsp)
-apply(tactic {* all_inj_repabs_tac @{context} 1*})
-apply(tactic {* clean_tac @{context} 1 *})
+apply(injection)
+apply(cleaning)
 done
 
 
@@ -203,9 +203,7 @@
 done
 
 lemma "foldl PLUS x [] = x"
-apply(tactic {* procedure_tac @{context} @{thm ho_tst} 1 *})
-apply(tactic {* regularize_tac @{context} 1 *})
-apply(tactic {* all_inj_repabs_tac @{context} 1*})
+apply(lifting rule: ho_tst)
 apply(tactic {* clean_tac @{context} 1 *})
 apply(simp only: foldl_prs[OF Quotient_my_int Quotient_my_int] nil_prs[OF Quotient_my_int])
 done
@@ -345,14 +343,10 @@
 done
 
 lemma "map (\<lambda>x. PLUS x ZERO) l = l"
-apply(tactic {* procedure_tac @{context} @{thm lam_tst4} 1 *})
-apply(tactic {* regularize_tac @{context} 1 *})
-apply(tactic {* all_inj_repabs_tac @{context} 1*})
-apply(tactic {* clean_tac @{context} 1*})
+apply(lifting rule: lam_tst4)
+apply(cleaning)
 apply(simp only: babs_prs[OF Quotient_my_int Quotient_my_int])
-apply(simp only: map_prs[OF Quotient_my_int Quotient_my_int])
-apply(tactic {* lambda_prs_tac @{context} 1 *})
-apply(rule refl)
+apply(simp only: map_prs[OF Quotient_my_int Quotient_my_int, symmetric])
 done
 
 end