equal
deleted
inserted
replaced
714 else |
714 else |
715 "" |
715 "" |
716 | _ => |
716 | _ => |
717 let |
717 let |
718 val preplay_msg = if preplay_fail |
718 val preplay_msg = if preplay_fail |
719 then "(!) proof may fail - preplaying was unsuccessful" |
719 then "may fail" |
720 else string_from_ext_time ext_time |
720 else string_from_ext_time ext_time |
721 val shrank_without_preplay_msg = |
721 val shrank_without_preplay_msg = |
722 "(!) proof may fail - shrank proof, but did not preplay" |
722 "may fail - shrank proof, but did not preplay" |
723 in |
723 in |
724 "\n\nStructured proof" |
724 "\n\nStructured proof" |
725 ^ (if verbose then |
725 ^ (if verbose then |
726 " (" ^ string_of_int num_steps |
726 " (" ^ string_of_int num_steps |
727 ^ " metis step" ^ plural_s num_steps |
727 ^ " metis step" ^ plural_s num_steps |