equal
deleted
inserted
replaced
46 fun RANGE_WARN tacs = RANGE (map WARN tacs) |
46 fun RANGE_WARN tacs = RANGE (map WARN tacs) |
47 |
47 |
48 fun atomize_thm thm = |
48 fun atomize_thm thm = |
49 let |
49 let |
50 val thm' = Thm.freezeT (forall_intr_vars thm) (* FIXME/TODO: is this proper Isar-technology? *) |
50 val thm' = Thm.freezeT (forall_intr_vars thm) (* FIXME/TODO: is this proper Isar-technology? *) |
51 val thm'' = ObjectLogic.atomize (cprop_of thm') |
51 val thm'' = Object_Logic.atomize (cprop_of thm') |
52 in |
52 in |
53 @{thm equal_elim_rule1} OF [thm'', thm'] |
53 @{thm equal_elim_rule1} OF [thm'', thm'] |
54 end |
54 end |
55 |
55 |
56 |
56 |
614 SOME (cterm_of thy inj_goal)] lifting_procedure_thm |
614 SOME (cterm_of thy inj_goal)] lifting_procedure_thm |
615 end |
615 end |
616 |
616 |
617 (* the tactic leaves three subgoals to be proved *) |
617 (* the tactic leaves three subgoals to be proved *) |
618 fun procedure_tac ctxt rthm = |
618 fun procedure_tac ctxt rthm = |
619 ObjectLogic.full_atomize_tac |
619 Object_Logic.full_atomize_tac |
620 THEN' gen_frees_tac ctxt |
620 THEN' gen_frees_tac ctxt |
621 THEN' SUBGOAL (fn (goal, i) => |
621 THEN' SUBGOAL (fn (goal, i) => |
622 let |
622 let |
623 val rthm' = atomize_thm rthm |
623 val rthm' = atomize_thm rthm |
624 val rule = procedure_inst ctxt (prop_of rthm') goal |
624 val rule = procedure_inst ctxt (prop_of rthm') goal |