diff -r 34d12737b379 -r d9151fa76f84 IntEx.thy --- 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 *})