147 |
147 |
148 val guess = (("guess", 0), propT); |
148 val guess = (("guess", 0), propT); |
149 val goal = Var guess; |
149 val goal = Var guess; |
150 val pos = Position.thread_data (); |
150 val pos = Position.thread_data (); |
151 fun print_result ctxt' (k, [(s, [_, th])]) = |
151 fun print_result ctxt' (k, [(s, [_, th])]) = |
152 Proof_Display.print_results int pos ctxt' (k, [(s, [th])]); |
152 Proof_Display.print_results {interactive = int, pos = pos, proof_state = true} |
|
153 ctxt' (k, [(s, [th])]); |
153 val before_qed = |
154 val before_qed = |
154 Method.primitive_text (fn ctxt => |
155 Method.primitive_text (fn ctxt => |
155 Goal.conclude #> Raw_Simplifier.norm_hhf ctxt #> |
156 Goal.conclude #> Raw_Simplifier.norm_hhf ctxt #> |
156 (fn th => Goal.protect 0 (Conjunction.intr (Drule.mk_term (Thm.cprop_of th)) th))); |
157 (fn th => Goal.protect 0 (Conjunction.intr (Drule.mk_term (Thm.cprop_of th)) th))); |
157 fun after_qed (result_ctxt, results) state' = |
158 fun after_qed (result_ctxt, results) state' = |