more standard SZS output
authorblanchet
Wed Apr 18 23:13:10 2012 +0200 (2012-04-18 ago)
changeset 475648074b18d8d76
parent 47563 01f687b84aff
child 47565 762eb0dacaa6
more standard SZS output
src/HOL/Tools/Nitpick/nitpick.ML
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick.ML	Wed Apr 18 22:40:25 2012 +0200
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick.ML	Wed Apr 18 23:13:10 2012 +0200
     1.3 @@ -693,7 +693,7 @@
     1.4                      | pretties => pstrs " for " @ pretties) @
     1.5                     [Pretty.str ":\n"])),
     1.6                Pretty.indent indent_size reconstructed_model]);
     1.7 -         print_t (fn () => "% SZS output stop");
     1.8 +         print_t (K "% SZS output end FiniteModel");
     1.9           if genuine then
    1.10             (if check_genuine andalso standard then
    1.11                case prove_hol_model scope tac_timeout free_names sel_names