--- a/IntEx.thy Fri Nov 27 09:16:32 2009 +0100
+++ b/IntEx.thy Fri Nov 27 10:04:49 2009 +0100
@@ -142,7 +142,7 @@
ML {*
fun lift_tac_fset lthy t =
- lift_tac lthy t [rel_eqv] rty [quot] trans2 rsp_thms defs
+ lift_tac lthy t [rel_eqv] rty [quot] rsp_thms defs
*}
lemma "PLUS a b = PLUS b a"
@@ -191,7 +191,7 @@
lemma "PLUS (PLUS i j) k = PLUS i (PLUS j k)"
apply(tactic {* procedure_tac @{context} @{thm plus_assoc_pre} 1 *})
apply(tactic {* regularize_tac @{context} [rel_eqv] [rel_refl] 1 *})
-apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} rty [quot] [rel_refl] trans2 rsp_thms) 1 *})
+apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} rty [quot] [rel_refl] [trans2] rsp_thms) 1 *})
oops