--- a/IntEx.thy	Sat Nov 28 04:37:30 2009 +0100
+++ b/IntEx.thy	Sat Nov 28 04:46:03 2009 +0100
@@ -147,11 +147,9 @@
 ML {* fun all_r_mk_comb_tac_intex lthy = all_r_mk_comb_tac lthy rty [quot] [rel_refl] [trans2] rsp_thms *}
 
 
-lemma cheat: "P" sorry
-
 lemma "PLUS a b = PLUS b a"
 apply(tactic {* procedure_tac @{context} @{thm plus_sym_pre} 1 *})
-apply(tactic {* regularize_tac @{context} [rel_eqv] [rel_refl] 1 *})
+apply(tactic {* regularize_tac @{context} rel_eqv [rel_refl] 1 *})
 prefer 2
 ML_prf {* val qtm = #concl (fst (Subgoal.focus @{context} 1 (#goal (Isar.goal ())))) *}
 ML_prf {* val aps = find_aps (prop_of (atomize_thm @{thm plus_sym_pre})) (term_of qtm) *}
@@ -161,12 +159,6 @@
 apply(tactic {* r_mk_comb_tac_intex @{context} 1*})
 apply(tactic {* r_mk_comb_tac_intex @{context} 1*})
 apply(tactic {* r_mk_comb_tac_intex @{context} 1*})
-apply(tactic {* r_mk_comb_tac_intex @{context} 1*}) (***)
-apply(tactic {* r_mk_comb_tac_intex @{context} 1*})
-apply(tactic {* r_mk_comb_tac_intex @{context} 1*})
-apply(tactic {* r_mk_comb_tac_intex @{context} 1*})
-apply(tactic {* r_mk_comb_tac_intex @{context} 1*})
-apply(tactic {* r_mk_comb_tac_intex @{context} 1*})
 apply(tactic {* r_mk_comb_tac_intex @{context} 1*})
 apply(tactic {* r_mk_comb_tac_intex @{context} 1*})
 apply(tactic {* r_mk_comb_tac_intex @{context} 1*})
@@ -178,7 +170,13 @@
 apply(tactic {* r_mk_comb_tac_intex @{context} 1*})
 apply(tactic {* r_mk_comb_tac_intex @{context} 1*})
 apply(tactic {* r_mk_comb_tac_intex @{context} 1*})
-apply(tactic {* all_r_mk_comb_tac_intex @{context} 1*})
+apply(tactic {* r_mk_comb_tac_intex @{context} 1*})
+apply(tactic {* r_mk_comb_tac_intex @{context} 1*})
+apply(tactic {* r_mk_comb_tac_intex @{context} 1*})
+apply(tactic {* r_mk_comb_tac_intex @{context} 1*})
+apply(tactic {* r_mk_comb_tac_intex @{context} 1*})
+apply(tactic {* r_mk_comb_tac_intex @{context} 1*})
+apply(tactic {* r_mk_comb_tac_intex @{context} 1*})
 done
 
 lemma plus_assoc_pre:
@@ -191,7 +189,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] [rel_refl] 1 *})
+apply(tactic {* regularize_tac @{context} rel_eqv [rel_refl] 1 *})
 apply(tactic {* all_r_mk_comb_tac_intex @{context} 1*}) 
 ML_prf {* val qtm = #concl (fst (Subgoal.focus @{context} 1 (#goal (Isar.goal ())))) *}
 ML_prf {* val aps = find_aps (prop_of (atomize_thm @{thm plus_sym_pre})) (term_of qtm) *}
@@ -228,7 +226,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 {* regularize_tac @{context} rel_eqv [rel_refl] 1 *})
 apply(tactic {* all_r_mk_comb_tac_intex @{context} 1*}) 
 ML_prf {* val qtm = #concl (fst (Subgoal.focus @{context} 1 (#goal (Isar.goal ())))) *}
 ML_prf {* val aps = find_aps (prop_of (atomize_thm @{thm plus_sym_pre})) (term_of qtm) *}