--- a/IntEx.thy	Sun Dec 06 11:39:34 2009 +0100
+++ b/IntEx.thy	Sun Dec 06 13:41:42 2009 +0100
@@ -12,6 +12,8 @@
   apply(auto simp add: mem_def expand_fun_eq)
   done
 
+thm quotient_equiv
+
 thm quotient_thm
 
 thm my_int_equivp
@@ -138,7 +140,7 @@
 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 [rel_eqv] *}
+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] *}
@@ -178,11 +180,9 @@
 done
 *)
 
-
-
 lemma "PLUS a b = PLUS a b"
 apply(tactic {* procedure_tac @{context} @{thm test1} 1 *})
-apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *})
+apply(tactic {* regularize_tac @{context} 1 *})
 apply(tactic {* all_inj_repabs_tac_intex @{context} 1*})
 apply(tactic {* clean_tac @{context} 1 *}) 
 done
@@ -214,7 +214,7 @@
 
 lemma "PLUS a b = PLUS b a"
 apply(tactic {* procedure_tac @{context} @{thm plus_sym_pre} 1 *})
-apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *})
+apply(tactic {* regularize_tac @{context} 1 *})
 apply(tactic {* all_inj_repabs_tac_intex @{context} 1*})
 apply(tactic {* clean_tac @{context} 1 *})
 done
@@ -229,7 +229,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} [rel_eqv] 1 *})
+apply(tactic {* regularize_tac @{context} 1 *})
 apply(tactic {* all_inj_repabs_tac_intex @{context} 1*})
 apply(tactic {* clean_tac @{context} 1 *})
 done
@@ -240,7 +240,7 @@
 
 lemma "foldl PLUS x [] = x"
 apply(tactic {* procedure_tac @{context} @{thm ho_tst} 1 *})
-apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *})
+apply(tactic {* regularize_tac @{context} 1 *})
 apply(tactic {* all_inj_repabs_tac_intex @{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])
@@ -251,7 +251,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} [rel_eqv] 1 *})
+apply(tactic {* regularize_tac @{context} 1 *})
 apply(tactic {* all_inj_repabs_tac_intex @{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])