diff -r ca37f4b6457c -r 8dfae5d97387 Quot/Examples/IntEx.thy
--- a/Quot/Examples/IntEx.thy	Tue Dec 08 11:17:56 2009 +0100
+++ b/Quot/Examples/IntEx.thy	Tue Dec 08 11:20:01 2009 +0100
@@ -136,15 +136,6 @@
   shows "(intrel ===> intrel ===> intrel) my_plus my_plus"
 by (simp)
 
-ML {* val qty = @{typ "my_int"} *}
-ML {* val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} qty *}
-ML {* val (trans2, reps_same, absrep, quot) = lookup_quot_thms @{context} "my_int"; *}
-
-ML {* fun lift_tac_intex lthy t = lift_tac lthy t *}
-
-ML {* fun inj_repabs_tac_intex lthy = inj_repabs_tac lthy [rel_refl] [trans2] *}
-ML {* fun all_inj_repabs_tac_intex lthy = all_inj_repabs_tac lthy [rel_refl] [trans2] *}
-
 lemma test1: "my_plus a b = my_plus a b"
 apply(rule refl)
 done
@@ -152,7 +143,7 @@
 lemma "PLUS a b = PLUS a b"
 apply(tactic {* procedure_tac @{context} @{thm test1} 1 *})
 apply(tactic {* regularize_tac @{context} 1 *})
-apply(tactic {* all_inj_repabs_tac_intex @{context} 1*})
+apply(tactic {* all_inj_repabs_tac @{context} 1*})
 apply(tactic {* clean_tac @{context} 1 *}) 
 done
 
@@ -168,7 +159,7 @@
 apply(rule ballI)
 apply(rule apply_rsp[OF Quotient_my_int plus_rsp])
 apply(simp only: in_respects)
-apply(tactic {* all_inj_repabs_tac_intex @{context} 1*})
+apply(tactic {* all_inj_repabs_tac @{context} 1*})
 apply(tactic {* clean_tac @{context} 1 *})
 done
 
@@ -180,7 +171,7 @@
 apply(tactic {* procedure_tac @{context} @{thm test3} 1 *})
 apply(rule impI)
 apply(rule plus_rsp)
-apply(tactic {* all_inj_repabs_tac_intex @{context} 1*})
+apply(tactic {* all_inj_repabs_tac @{context} 1*})
 apply(tactic {* clean_tac @{context} 1 *})
 done
 
@@ -188,7 +179,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_intex @{context} 1*})
+apply(tactic {* all_inj_repabs_tac @{context} 1*})
 apply(tactic {* clean_tac @{context} 1 *})
 done
 
@@ -203,7 +194,7 @@
 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_intex @{context} 1*})
+apply(tactic {* all_inj_repabs_tac @{context} 1*})
 apply(tactic {* clean_tac @{context} 1 *})
 done
 
@@ -214,7 +205,7 @@
 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_intex @{context} 1*})
+apply(tactic {* all_inj_repabs_tac @{context} 1*})
 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
@@ -225,7 +216,7 @@
 lemma "foldl PLUS x (h # t) = PLUS h (foldl PLUS x t)"
 apply(tactic {* procedure_tac @{context} @{thm ho_tst2} 1 *})
 apply(tactic {* regularize_tac @{context} 1 *})
-apply(tactic {* all_inj_repabs_tac_intex @{context} 1*})
+apply(tactic {* all_inj_repabs_tac @{context} 1*})
 apply(tactic {* clean_tac @{context} 1 *})
 apply(simp only: foldl_prs[OF Quotient_my_int Quotient_my_int] cons_prs[OF Quotient_my_int])
 done
@@ -236,7 +227,7 @@
 lemma "foldl f (x::my_int) ([]::my_int list) = x"
 apply(tactic {* procedure_tac @{context} @{thm ho_tst3} 1 *})
 apply(tactic {* regularize_tac @{context} 1 *})
-apply(tactic {* all_inj_repabs_tac_intex @{context} 1*})
+apply(tactic {* all_inj_repabs_tac @{context} 1*})
 (* TODO: does not work when this is added *)
 (* apply(tactic {* lambda_prs_tac @{context} 1 *})*)
 apply(tactic {* clean_tac @{context} 1 *})
@@ -249,7 +240,7 @@
 lemma "(\<lambda>x. (x, x)) (y::my_int) = (y, y)"
 apply(tactic {* procedure_tac @{context} @{thm lam_tst} 1 *})
 apply(tactic {* regularize_tac @{context} 1 *})
-apply(tactic {* all_inj_repabs_tac_intex @{context} 1*})
+apply(tactic {* all_inj_repabs_tac @{context} 1*})
 apply(tactic {* clean_tac @{context} 1 *})
 apply(simp add: pair_prs)
 done
@@ -325,7 +316,7 @@
 lemma "(\<lambda>(y :: my_int). y) = (\<lambda>(x :: my_int). x)"
 apply(tactic {* procedure_tac @{context} @{thm lam_tst3a} 1 *})
 defer
-apply(tactic {* all_inj_repabs_tac_intex @{context} 1*})
+apply(tactic {* all_inj_repabs_tac @{context} 1*})
 apply(tactic {* clean_tac  @{context} 1 *})
 apply(subst babs_rsp)
 apply(tactic {* clean_tac  @{context} 1 *})
@@ -343,7 +334,7 @@
 lemma "(\<lambda>(y :: my_int => my_int). y) = (\<lambda>(x :: my_int => my_int). x)"
 apply(tactic {* procedure_tac @{context} @{thm lam_tst3b} 1 *})
 defer
-apply(tactic {* all_inj_repabs_tac_intex @{context} 1*})
+apply(tactic {* all_inj_repabs_tac @{context} 1*})
 apply(tactic {* clean_tac  @{context} 1 *})
 apply(subst babs_rsp)
 apply(tactic {* clean_tac  @{context} 1 *})