equal
deleted
inserted
replaced
27 (* canonical proof decomposition -- similar to fix/assume/show *) |
27 (* canonical proof decomposition -- similar to fix/assume/show *) |
28 |
28 |
29 fun focus ctxt i st = |
29 fun focus ctxt i st = |
30 let |
30 let |
31 val ((schematics, [st']), ctxt') = |
31 val ((schematics, [st']), ctxt') = |
32 Variable.import_thms true [Simplifier.norm_hhf_protect st] ctxt; |
32 Variable.import true [Simplifier.norm_hhf_protect st] ctxt; |
33 val ((params, goal), ctxt'') = Variable.focus_subgoal i st' ctxt'; |
33 val ((params, goal), ctxt'') = Variable.focus_subgoal i st' ctxt'; |
34 val asms = Drule.strip_imp_prems goal; |
34 val asms = Drule.strip_imp_prems goal; |
35 val concl = Drule.strip_imp_concl goal; |
35 val concl = Drule.strip_imp_concl goal; |
36 val (prems, context) = Assumption.add_assumes asms ctxt''; |
36 val (prems, context) = Assumption.add_assumes asms ctxt''; |
37 in |
37 in |