src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
changeset 54140 564b8adb0952
parent 54131 18b23d787062
child 54141 f57f8e7a879f
equal deleted inserted replaced
54139:c8ea98c1f4b2 54140:564b8adb0952
  1199                 |> fold relearn_old_fact old_facts
  1199                 |> fold relearn_old_fact old_facts
  1200             in commit true [] relearns flops; n end
  1200             in commit true [] relearns flops; n end
  1201       in
  1201       in
  1202         if verbose orelse auto_level < 2 then
  1202         if verbose orelse auto_level < 2 then
  1203           "Learned " ^ string_of_int n ^ " nontrivial " ^
  1203           "Learned " ^ string_of_int n ^ " nontrivial " ^
  1204           (if run_prover then "automatic" else "Isar") ^ " proof" ^ plural_s n ^
  1204           (if run_prover then "automatic and " else "") ^ "Isar proof" ^ plural_s n ^
  1205           (if verbose then " in " ^ string_of_time (Timer.checkRealTimer timer)
  1205           (if verbose then " in " ^ string_of_time (Timer.checkRealTimer timer)
  1206            else "") ^ "."
  1206            else "") ^ "."
  1207         else
  1207         else
  1208           ""
  1208           ""
  1209       end
  1209       end