--- a/IntEx.thy	Sat Dec 05 00:06:27 2009 +0100
+++ b/IntEx.thy	Sat Dec 05 13:49:35 2009 +0100
@@ -149,6 +149,36 @@
 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
+
+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 {* inj_repabs_tac_intex @{context} 1*})
+(* does not work yet *)
+oops
+
+lemma test2: "my_plus a = my_plus a"
+apply(rule refl)
+done
+
+lemma "PLUS a = PLUS a"
+apply(tactic {* procedure_tac @{context} @{thm test2} 1 *})
+(* does not work yet *)
+oops
+
+lemma test3: "my_plus = my_plus"
+apply(rule refl)
+done
+
+lemma "PLUS = PLUS"
+apply(tactic {* procedure_tac @{context} @{thm test3} 1 *})
+apply(rule ho_plus_rsp)
+(* does not work yet *)
+oops
+
 
 lemma "PLUS a b = PLUS b a"
 apply(tactic {* procedure_tac @{context} @{thm plus_sym_pre} 1 *})