equal
deleted
inserted
replaced
78 --- (finish) |
78 --- (finish) |
79 C |
79 C |
80 *) |
80 *) |
81 fun check_finished ctxt th = |
81 fun check_finished ctxt th = |
82 if Thm.no_prems th then th |
82 if Thm.no_prems th then th |
83 else |
83 else raise THM ("Proof failed.\n" ^ Goal_Display.string_of_goal ctxt th, 0, [th]); |
84 raise THM ("Proof failed.\n" ^ Pretty.string_of (Goal_Display.pretty_goal ctxt th), 0, [th]); |
|
85 |
84 |
86 fun finish ctxt = check_finished ctxt #> conclude; |
85 fun finish ctxt = check_finished ctxt #> conclude; |
87 |
86 |
88 |
87 |
89 |
88 |