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