equal
deleted
inserted
replaced
273 |
273 |
274 fun levels_up 0 = "" |
274 fun levels_up 0 = "" |
275 | levels_up i = " (" ^ string_of_int i ^ " levels up)"; |
275 | levels_up i = " (" ^ string_of_int i ^ " levels up)"; |
276 |
276 |
277 fun print_goal (i, ((kind, name, _, _), (_, thm))) = |
277 fun print_goal (i, ((kind, name, _, _), (_, thm))) = |
278 (writeln (kind_name kind ^ " " ^ quote name ^ levels_up (i div 1) ^ ":"); (* FIXME *) |
278 (writeln (kind_name kind ^ " " ^ quote name ^ levels_up (i div 2) ^ ":"); |
279 Locale.print_goals_marker begin_goal (! goals_limit) thm); |
279 Locale.print_goals_marker begin_goal (! goals_limit) thm); |
280 in |
280 in |
281 writeln ("Nesting level: " ^ string_of_int (length nodes div 1)); (* FIXME *) |
281 writeln ("Nesting level: " ^ string_of_int (length nodes div 2)); |
282 writeln ""; |
282 writeln ""; |
283 writeln (mode_name mode ^ " mode"); |
283 writeln (mode_name mode ^ " mode"); |
284 writeln ""; |
284 writeln ""; |
285 ProofContext.print_context context; |
285 ProofContext.print_context context; |
286 writeln ""; |
286 writeln ""; |