equal
deleted
inserted
replaced
363 val prt_ctxt = |
363 val prt_ctxt = |
364 if verbose orelse mode = Forward then Proof_Context.pretty_context ctxt |
364 if verbose orelse mode = Forward then Proof_Context.pretty_context ctxt |
365 else if mode = Backward then Proof_Context.pretty_ctxt ctxt |
365 else if mode = Backward then Proof_Context.pretty_ctxt ctxt |
366 else []; |
366 else []; |
367 in |
367 in |
368 [Pretty.str ("proof (" ^ mode_name mode ^ "): step " ^ string_of_int nr ^ |
368 [Pretty.str ("proof (" ^ mode_name mode ^ "): depth " ^ string_of_int (level state div 2 - 1)), |
369 (if verbose then ", depth " ^ string_of_int (level state div 2 - 1) else "")), |
|
370 Pretty.str ""] @ |
369 Pretty.str ""] @ |
371 (if null prt_ctxt then [] else prt_ctxt @ [Pretty.str ""]) @ |
370 (if null prt_ctxt then [] else prt_ctxt @ [Pretty.str ""]) @ |
372 (if verbose orelse mode = Forward then |
371 (if verbose orelse mode = Forward then |
373 pretty_facts ctxt "" facts @ prt_goal (try find_goal state) |
372 pretty_facts ctxt "" facts @ prt_goal (try find_goal state) |
374 else if mode = Chain then pretty_facts ctxt "picking" facts |
373 else if mode = Chain then pretty_facts ctxt "picking" facts |