| changeset 29393 | bc41c9cbbfc2 |
| parent 29385 | c96b91bab2e6 |
| child 29417 | 438c39fc93c8 |
| 29392:4638ab6c878f | 29393:bc41c9cbbfc2 |
|---|---|
343 |
343 |
344 fun description strs = |
344 fun description strs = |
345 (case filter_out (fn s => s = "") strs of [] => "" |
345 (case filter_out (fn s => s = "") strs of [] => "" |
346 | strs' => enclose " (" ")" (commas strs')); |
346 | strs' => enclose " (" ")" (commas strs')); |
347 |
347 |
348 fun prt_goal (SOME (ctxt, (i, {statement = ((_, pos), _, _), messages, using, goal, ...}))) = |
348 fun prt_goal (SOME (ctxt, (i, {statement = ((_, pos), _, _), messages, using, goal, before_qed, after_qed}))) = |
349 pretty_facts "using " ctxt |
349 pretty_facts "using " ctxt |
350 (if mode <> Backward orelse null using then NONE else SOME using) @ |
350 (if mode <> Backward orelse null using then NONE else SOME using) @ |
351 [Pretty.str ("goal" ^ |
351 [Pretty.str ("goal" ^ |
352 description [levels_up (i div 2), subgoals (Thm.nprems_of goal)] ^ ":")] @ |
352 description [levels_up (i div 2), subgoals (Thm.nprems_of goal)] ^ ":")] @ |
353 pretty_goals_local ctxt Markup.subgoal |
353 pretty_goals_local ctxt Markup.subgoal |