diff -r cc0b9cb367cd -r 9cb45d022524 IntEx.thy --- a/IntEx.thy Sun Nov 29 19:48:55 2009 +0100 +++ b/IntEx.thy Sun Nov 29 23:59:37 2009 +0100 @@ -153,6 +153,9 @@ 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) *} apply(tactic {* clean_tac @{context} [quot] defs aps 1 *}) +apply(simp add: id_def) +apply(tactic {* inj_repabs_tac_intex @{context} 1*}) +apply(tactic {* inj_repabs_tac_intex @{context} 1*}) apply(tactic {* inj_repabs_tac_intex @{context} 1*}) apply(tactic {* inj_repabs_tac_intex @{context} 1*}) apply(tactic {* inj_repabs_tac_intex @{context} 1*}) @@ -189,6 +192,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(simp) apply(tactic {* all_inj_repabs_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) *} @@ -227,6 +231,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] 1 *}) +apply(simp) apply(tactic {* all_inj_repabs_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) *}