equal
deleted
inserted
replaced
140 ML {* val (trans2, reps_same, absrep, quot) = lookup_quot_thms @{context} "my_int"; *} |
140 ML {* val (trans2, reps_same, absrep, quot) = lookup_quot_thms @{context} "my_int"; *} |
141 ML {* val consts = lookup_quot_consts defs *} |
141 ML {* val consts = lookup_quot_consts defs *} |
142 |
142 |
143 ML {* |
143 ML {* |
144 fun lift_tac_fset lthy t = |
144 fun lift_tac_fset lthy t = |
145 lift_tac lthy t [rel_eqv] rty [quot] trans2 rsp_thms defs |
145 lift_tac lthy t [rel_eqv] rty [quot] rsp_thms defs |
146 *} |
146 *} |
147 |
147 |
148 lemma "PLUS a b = PLUS b a" |
148 lemma "PLUS a b = PLUS b a" |
149 by (tactic {* lift_tac_fset @{context} @{thm plus_sym_pre} 1 *}) |
149 by (tactic {* lift_tac_fset @{context} @{thm plus_sym_pre} 1 *}) |
150 |
150 |
189 *} |
189 *} |
190 |
190 |
191 lemma "PLUS (PLUS i j) k = PLUS i (PLUS j k)" |
191 lemma "PLUS (PLUS i j) k = PLUS i (PLUS j k)" |
192 apply(tactic {* procedure_tac @{context} @{thm plus_assoc_pre} 1 *}) |
192 apply(tactic {* procedure_tac @{context} @{thm plus_assoc_pre} 1 *}) |
193 apply(tactic {* regularize_tac @{context} [rel_eqv] [rel_refl] 1 *}) |
193 apply(tactic {* regularize_tac @{context} [rel_eqv] [rel_refl] 1 *}) |
194 apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} rty [quot] [rel_refl] trans2 rsp_thms) 1 *}) |
194 apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} rty [quot] [rel_refl] [trans2] rsp_thms) 1 *}) |
195 oops |
195 oops |
196 |
196 |
197 |
197 |
198 (* |
198 (* |
199 |
199 |