tuned print_state;
authorwenzelm
Sun Nov 29 13:20:49 1998 +0100 (1998-11-29)
changeset 5993d03fbef54c62
parent 5992 263051aaf0de
child 5994 7b84677315ed
tuned print_state;
changed solve semantics: support back-pressure of asms (cut, def etc.);
src/Pure/Isar/proof.ML
     1.1 --- a/src/Pure/Isar/proof.ML	Sun Nov 29 13:19:48 1998 +0100
     1.2 +++ b/src/Pure/Isar/proof.ML	Sun Nov 29 13:20:49 1998 +0100
     1.3 @@ -282,12 +282,12 @@
     1.4    in
     1.5      writeln ("Nesting level: " ^ string_of_int (length nodes div 1));	(* FIXME *)
     1.6      writeln "";
     1.7 +    writeln (mode_name mode ^ " mode");
     1.8 +    writeln "";
     1.9      ProofContext.print_context context;
    1.10      writeln "";
    1.11      print_facts facts;
    1.12 -    print_goal (find_goal 0 state);
    1.13 -    writeln "";
    1.14 -    writeln (mode_name mode ^ " mode")
    1.15 +    print_goal (find_goal 0 state)
    1.16    end;
    1.17  
    1.18  
    1.19 @@ -406,7 +406,7 @@
    1.20  fun solve_goal rule state =
    1.21    let
    1.22      val (_, (result, (facts, thm))) = find_goal 0 state;
    1.23 -    val thms' = FIRSTGOAL (solve_tac [rule]) thm;
    1.24 +    val thms' = FIRSTGOAL (rtac rule THEN_ALL_NEW (TRY o assume_tac)) thm;
    1.25    in Seq.map (fn thm' => map_goal (K (result, (facts, thm'))) state) thms' end;
    1.26  
    1.27