138 ML {* val defs = @{thms PLUS_def} *} |
138 ML {* val defs = @{thms PLUS_def} *} |
139 ML {* val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} qty *} |
139 ML {* val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} qty *} |
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 {* fun lift_tac_intex lthy t = lift_tac lthy t [rel_eqv] rty [quot] defs *} |
143 ML {* fun lift_tac_intex lthy t = lift_tac lthy t [rel_eqv] [quot] defs *} |
144 |
144 |
145 ML {* fun inj_repabs_tac_intex lthy = inj_repabs_tac lthy rty [quot] [rel_refl] [trans2] *} |
145 ML {* fun inj_repabs_tac_intex lthy = inj_repabs_tac lthy [quot] [rel_refl] [trans2] *} |
146 ML {* fun all_inj_repabs_tac_intex lthy = all_inj_repabs_tac lthy rty [quot] [rel_refl] [trans2] *} |
146 ML {* fun all_inj_repabs_tac_intex lthy = all_inj_repabs_tac lthy [quot] [rel_refl] [trans2] *} |
147 |
147 |
148 |
148 |
149 lemma "PLUS a b = PLUS b a" |
149 lemma "PLUS a b = PLUS b a" |
150 apply(tactic {* procedure_tac @{context} @{thm plus_sym_pre} 1 *}) |
150 apply(tactic {* procedure_tac @{context} @{thm plus_sym_pre} 1 *}) |
151 apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *}) |
151 apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *}) |