src/HOL/Tools/Nitpick/nitpick.ML
changeset 47562 a72239723ae8
parent 47560 e30323bfc93c
child 47564 8074b18d8d76
     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 22:40:25 2012 +0200
     1.3 @@ -680,7 +680,7 @@
     1.4                  if falsify then "CounterSatisfiable" else "Satisfiable"
     1.5                else
     1.6                  "Unknown") ^ "\n" ^
     1.7 -             "% SZS output start FiniteModel\n");
     1.8 +             "% SZS output start FiniteModel");
     1.9           pprint_a (Pretty.chunks
    1.10               [Pretty.blk (0,
    1.11                    (pstrs ((if mode = Auto_Try then "Auto " else "") ^
    1.12 @@ -693,7 +693,7 @@
    1.13                      | pretties => pstrs " for " @ pretties) @
    1.14                     [Pretty.str ":\n"])),
    1.15                Pretty.indent indent_size reconstructed_model]);
    1.16 -         print_t (fn () => "% SZS output stop\n");
    1.17 +         print_t (fn () => "% SZS output stop");
    1.18           if genuine then
    1.19             (if check_genuine andalso standard then
    1.20                case prove_hol_model scope tac_timeout free_names sel_names
    1.21 @@ -1005,7 +1005,7 @@
    1.22            (print_nt (fn () => excipit "checked"); unknownN)
    1.23          else if max_genuine = original_max_genuine then
    1.24            if max_potential = original_max_potential then
    1.25 -            (print_t (K "% SZS status Unknown\n");
    1.26 +            (print_t (K "% SZS status Unknown");
    1.27               print_nt (fn () =>
    1.28                   "Nitpick found no " ^ das_wort_model ^ "." ^
    1.29                   (if not standard andalso likely_in_struct_induct_step then