equal
deleted
inserted
replaced
185 val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} @{typ "my_int"} |
185 val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} @{typ "my_int"} |
186 val (trans2, reps_same, absrep, quot) = lookup_quot_thms @{context} "my_int" |
186 val (trans2, reps_same, absrep, quot) = lookup_quot_thms @{context} "my_int" |
187 *} |
187 *} |
188 |
188 |
189 |
189 |
190 lemma "\<forall>i j k. PLUS (PLUS i j) k = PLUS i (PLUS j k)" |
190 lemma "PLUS (PLUS i j) k = PLUS i (PLUS j k)" |
191 apply(tactic {* procedure_tac @{thm plus_assoc_pre} @{context} 1 *}) |
191 apply(tactic {* procedure_tac @{thm plus_assoc_pre} @{context} 1 *}) |
192 apply(tactic {* regularize_tac @{context} rel_eqv rel_refl 1 *}) |
192 apply(tactic {* regularize_tac @{context} rel_eqv rel_refl 1 *}) |
193 apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms) 1 *}) |
193 apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms) 1 *}) |
194 apply(tactic {* clean_tac @{context} quot @{thms PLUS_def} reps_same 1 *}) |
194 apply(tactic {* clean_tac @{context} quot @{thms PLUS_def} reps_same 1 *}) |
195 done |
195 done |