equal
deleted
inserted
replaced
295 ML {* val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} qty *} |
295 ML {* val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} qty *} |
296 ML {* val (trans2, reps_same, absrep, quot) = lookup_quot_thms @{context} "fset"; *} |
296 ML {* val (trans2, reps_same, absrep, quot) = lookup_quot_thms @{context} "fset"; *} |
297 ML {* fun lift_tac_fset lthy t = lift_tac lthy t [rel_eqv] *} |
297 ML {* fun lift_tac_fset lthy t = lift_tac lthy t [rel_eqv] *} |
298 |
298 |
299 lemma "IN x EMPTY = False" |
299 lemma "IN x EMPTY = False" |
300 |
|
301 apply(tactic {* (ObjectLogic.full_atomize_tac |
|
302 THEN' gen_frees_tac @{context}) 1 *}) |
|
303 |
|
304 apply(tactic {* procedure_tac @{context} @{thm m1} 1 *}) |
300 apply(tactic {* procedure_tac @{context} @{thm m1} 1 *}) |
305 apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *}) |
301 apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *}) |
306 apply(tactic {* all_inj_repabs_tac @{context} [rel_refl] [trans2] 1 *}) |
302 apply(tactic {* all_inj_repabs_tac @{context} [rel_refl] [trans2] 1 *}) |
307 apply(tactic {* clean_tac @{context} 1*}) |
303 apply(tactic {* clean_tac @{context} 1*}) |
308 done |
304 done |