equal
deleted
inserted
replaced
329 |
329 |
330 fun description strs = |
330 fun description strs = |
331 (case filter_out (equal "") strs of [] => "" |
331 (case filter_out (equal "") strs of [] => "" |
332 | strs' => enclose " (" ")" (commas strs')); |
332 | strs' => enclose " (" ")" (commas strs')); |
333 |
333 |
334 fun prt_goal (SOME (ctxt, (i, {using, goal, before_qed, after_qed, ...}))) = |
334 fun prt_goal (SOME (ctxt, (i, {statement = _, using, goal, before_qed, after_qed}))) = |
335 pretty_facts "using " ctxt |
335 pretty_facts "using " ctxt |
336 (if mode <> Backward orelse null using then NONE else SOME using) @ |
336 (if mode <> Backward orelse null using then NONE else SOME using) @ |
337 [Pretty.str ("goal" ^ |
337 [Pretty.str ("goal" ^ |
338 description [levels_up (i div 2), subgoals (Thm.nprems_of goal)] ^ ":")] @ |
338 description [levels_up (i div 2), subgoals (Thm.nprems_of goal)] ^ ":")] @ |
339 pretty_goals_local ctxt bg (true, ! show_main_goal) (! Display.goals_limit) goal |
339 pretty_goals_local ctxt bg (true, ! show_main_goal) (! Display.goals_limit) goal |