--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Sun Aug 14 12:26:09 2016 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Sun Aug 14 12:26:09 2016 +0200
@@ -301,7 +301,7 @@
let
fun default_prover_name () =
hd (#provers (Sledgehammer_Commands.default_params thy []))
- handle List.Empty => error "No ATP available."
+ handle List.Empty => error "No ATP available"
in
(case AList.lookup (op =) args proverK of
SOME name => name
--- a/src/HOL/TPTP/mash_eval.ML Sun Aug 14 12:26:09 2016 +0200
+++ b/src/HOL/TPTP/mash_eval.ML Sun Aug 14 12:26:09 2016 +0200
@@ -88,11 +88,11 @@
val name =
(case names |> filter (curry (op <>) "") |> distinct (op =) of
[name] => name
- | names => error ("Input files out of sync: facts " ^ commas (map quote names) ^ "."))
+ | names => error ("Input files out of sync: facts " ^ commas (map quote names)))
val th =
case find_first (fn (_, th) => nickname_of_thm th = name) facts of
SOME (_, th) => th
- | NONE => error ("No fact called \"" ^ name ^ "\".")
+ | NONE => error ("No fact called \"" ^ name)
val goal = goal_of_thm (Proof_Context.theory_of ctxt) th
val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal goal 1 ctxt
val isar_deps = these (isar_dependencies_of name_tabs th)
--- a/src/HOL/TPTP/mash_export.ML Sun Aug 14 12:26:09 2016 +0200
+++ b/src/HOL/TPTP/mash_export.ML Sun Aug 14 12:26:09 2016 +0200
@@ -310,7 +310,7 @@
val (name', mepo_suggs) =
extract_suggestions mepo_line
||> (map fst #> weight_facts_steeply)
- val _ = if name = name' then () else error "Input files out of sync."
+ val _ = if name = name' then () else error "Input files out of sync"
val mess =
[(mepo_weight, (mepo_suggs, [])),
(mash_weight, (mash_suggs, []))]
@@ -322,7 +322,7 @@
val mepo_lines = Path.explode mepo_file_name |> File.read_lines
in
if length mash_lines = length mepo_lines then List.app do_fact (mash_lines ~~ mepo_lines)
- else warning "Skipped: MaSh file missing or out of sync with MePo file."
+ else warning "Skipped: MaSh file missing or out of sync with MePo file"
end
end;
--- a/src/HOL/Tools/ATP/atp_problem_generate.ML Sun Aug 14 12:26:09 2016 +0200
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML Sun Aug 14 12:26:09 2016 +0200
@@ -666,7 +666,7 @@
| ("erased", (NONE, All_Types (* naja *))) =>
Guards (Raw_Polymorphic With_Phantom_Type_Vars, No_Types)
| _ => raise Same.SAME))
- handle Same.SAME => error ("Unknown type encoding: " ^ quote s ^ ".")
+ handle Same.SAME => error ("Unknown type encoding: " ^ quote s)
fun adjust_order THF_Without_Choice (Higher_Order _) =
Higher_Order THF_Without_Choice
@@ -1803,7 +1803,7 @@
else if lam_trans = keep_lamsN then
map (Envir.eta_contract) #> rpair []
else
- error ("Unknown lambda translation scheme: " ^ quote lam_trans ^ ".")
+ error ("Unknown lambda translation scheme: " ^ quote lam_trans)
val pull_and_reorder_definitions =
let
--- a/src/HOL/Tools/ATP/atp_proof.ML Sun Aug 14 12:26:09 2016 +0200
+++ b/src/HOL/Tools/ATP/atp_proof.ML Sun Aug 14 12:26:09 2016 +0200
@@ -173,44 +173,41 @@
""
val missing_message_tail =
- " appears to be missing. You will need to install it if you want to invoke \
- \remote provers."
+ " appears to be missing; you will need to install it if you want to invoke \
+ \remote provers"
fun from_lemmas [] = ""
| from_lemmas ss = " from " ^ space_implode " " (Try.serial_commas "and" (map quote ss))
-fun string_of_atp_failure MaybeUnprovable = "The generated problem is maybe unprovable."
- | string_of_atp_failure Unprovable = "The generated problem is unprovable."
- | string_of_atp_failure GaveUp = "The prover gave up."
+fun string_of_atp_failure MaybeUnprovable = "The generated problem is maybe unprovable"
+ | string_of_atp_failure Unprovable = "The generated problem is unprovable"
+ | string_of_atp_failure GaveUp = "The prover gave up"
| string_of_atp_failure ProofMissing =
- "The prover claims the conjecture is a theorem but did not provide a proof."
+ "The prover claims the conjecture is a theorem but did not provide a proof"
| string_of_atp_failure ProofIncomplete =
- "The prover claims the conjecture is a theorem but provided an incomplete proof."
+ "The prover claims the conjecture is a theorem but provided an incomplete proof"
| string_of_atp_failure ProofUnparsable =
- "The prover claims the conjecture is a theorem but provided an unparsable proof."
+ "The prover claims the conjecture is a theorem but provided an unparsable proof"
| string_of_atp_failure (UnsoundProof (false, ss)) =
"The prover derived \"False\"" ^ from_lemmas ss ^
- ". Specify a sound type encoding or omit the \"type_enc\" option."
+ "; specify a sound type encoding or omit the \"type_enc\" option"
| string_of_atp_failure (UnsoundProof (true, ss)) =
"The prover derived \"False\"" ^ from_lemmas ss ^
- ". This could be due to inconsistent axioms (including \"sorry\"s) or to \
- \a bug in Sledgehammer. If the problem persists, please contact the \
- \Isabelle developers."
- | string_of_atp_failure CantConnect = "Cannot connect to server."
- | string_of_atp_failure TimedOut = "Timed out."
+ ", which could be due to inconsistent axioms (including \"sorry\"s) or to \
+ \a bug in Sledgehammer"
+ | string_of_atp_failure CantConnect = "Cannot connect to server"
+ | string_of_atp_failure TimedOut = "Timed out"
| string_of_atp_failure Inappropriate =
- "The generated problem lies outside the prover's scope."
- | string_of_atp_failure OutOfResources = "The prover ran out of resources."
+ "The generated problem lies outside the prover's scope"
+ | string_of_atp_failure OutOfResources = "The prover ran out of resources"
| string_of_atp_failure NoPerl = "Perl" ^ missing_message_tail
| string_of_atp_failure NoLibwwwPerl =
"The Perl module \"libwww-perl\"" ^ missing_message_tail
- | string_of_atp_failure MalformedInput =
- "The generated problem is malformed. Please report this to the Isabelle \
- \developers."
- | string_of_atp_failure MalformedOutput = "The prover output is malformed."
- | string_of_atp_failure Interrupted = "The prover was interrupted."
- | string_of_atp_failure Crashed = "The prover crashed."
- | string_of_atp_failure InternalError = "An internal prover error occurred."
+ | string_of_atp_failure MalformedInput = "The generated problem is malformed"
+ | string_of_atp_failure MalformedOutput = "The prover output is malformed"
+ | string_of_atp_failure Interrupted = "The prover was interrupted"
+ | string_of_atp_failure Crashed = "The prover crashed"
+ | string_of_atp_failure InternalError = "An internal prover error occurred"
| string_of_atp_failure (UnknownError s) =
"A prover error occurred" ^
(if s = "" then ". (Pass the \"verbose\" option for details.)"
--- a/src/HOL/Tools/ATP/atp_proof_reconstruct.ML Sun Aug 14 12:26:09 2016 +0200
+++ b/src/HOL/Tools/ATP/atp_proof_reconstruct.ML Sun Aug 14 12:26:09 2016 +0200
@@ -271,7 +271,7 @@
| ATerm ((s, tys), us) =>
if s = ""
then error "Isar proof reconstruction failed because the ATP proof \
- \contains unparsable material."
+ \contains unparsable material"
else if s = tptp_equal then
list_comb (Const (@{const_name HOL.eq}, Type_Infer.anyT @{sort type}),
map (do_term NONE) us)
@@ -349,7 +349,7 @@
ATerm ((s, tys), us) =>
if s = "" then
error "Isar proof reconstruction failed because the ATP proof contains unparsable \
- \material."
+ \material"
else if String.isPrefix native_type_prefix s then
@{const True} (* ignore TPTP type information (needed?) *)
else if s = tptp_equal then
@@ -428,10 +428,10 @@
fun term_of_atp ctxt (ATP_Problem.THF _) type_enc =
if ATP_Problem_Generate.is_type_enc_higher_order type_enc then K (term_of_atp_ho ctxt)
- else error "Unsupported Isar reconstruction."
+ else error "Unsupported Isar reconstruction"
| term_of_atp ctxt _ type_enc =
if not (ATP_Problem_Generate.is_type_enc_higher_order type_enc) then term_of_atp_fo ctxt
- else error "Unsupported Isar reconstruction."
+ else error "Unsupported Isar reconstruction"
fun term_of_atom ctxt format type_enc textual sym_tab pos (u as ATerm ((s, _), _)) =
if String.isPrefix class_prefix s then
--- a/src/HOL/Tools/ATP/atp_satallax.ML Sun Aug 14 12:26:09 2016 +0200
+++ b/src/HOL/Tools/ATP/atp_satallax.ML Sun Aug 14 12:26:09 2016 +0200
@@ -122,7 +122,7 @@
group_by_pair new_goals generated_assumptions
end
else
- raise Fail ("the rule " ^ rule ^" is not supported in the reconstruction.")
+ raise Fail ("the rule " ^ rule ^" is not supported in the reconstruction")
end
fun to_satallax_step (((id, role), formula), (SOME (_,((rule, l), used_rules)))) =
let
--- a/src/HOL/Tools/ATP/atp_systems.ML Sun Aug 14 12:26:09 2016 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML Sun Aug 14 12:26:09 2016 +0200
@@ -139,7 +139,7 @@
val extend = I
fun merge data : T =
Symtab.merge (eq_snd (op =)) data
- handle Symtab.DUP name => error ("Duplicate ATP: " ^ quote name ^ ".")
+ handle Symtab.DUP name => error ("Duplicate ATP: " ^ quote name)
)
fun to_secs min time = Int.max (min, (Time.toMilliseconds time + 999) div 1000)
@@ -640,7 +640,7 @@
(warning
(case extract_known_atp_failure known_perl_failures output of
SOME failure => string_of_atp_failure failure
- | NONE => trim_line output ^ "."); []))) ()
+ | NONE => trim_line output); []))) ()
handle Timeout.TIMEOUT _ => []
fun find_remote_system name [] systems =
@@ -658,11 +658,11 @@
fun the_remote_system name versions =
(case get_remote_system name versions of
(SOME sys, _) => sys
- | (NONE, []) => error "SystemOnTPTP is not available."
+ | (NONE, []) => error "SystemOnTPTP is currently not available"
| (NONE, syss) =>
(case syss |> filter_out (String.isPrefix "%") |> filter_out (curry (op =) "") of
- [] => error "SystemOnTPTP is currently not available."
- | [msg] => error ("SystemOnTPTP is currently not available: " ^ msg ^ ".")
+ [] => error "SystemOnTPTP is currently not available"
+ | [msg] => error ("SystemOnTPTP is currently not available: " ^ msg)
| syss =>
error ("System " ^ quote name ^ " is not available at SystemOnTPTP.\n(Available systems: " ^
commas_quote syss ^ ".)")))
@@ -744,11 +744,11 @@
fun add_atp (name, config) thy =
Data.map (Symtab.update_new (name, (config, stamp ()))) thy
- handle Symtab.DUP name => error ("Duplicate ATP: " ^ quote name ^ ".")
+ handle Symtab.DUP name => error ("Duplicate ATP: " ^ quote name)
fun get_atp thy name =
fst (the (Symtab.lookup (Data.get thy) name))
- handle Option.Option => error ("Unknown ATP: " ^ name ^ ".")
+ handle Option.Option => error ("Unknown ATP: " ^ name)
val supported_atps = Symtab.keys o Data.get
--- a/src/HOL/Tools/Sledgehammer/async_manager_legacy.ML Sun Aug 14 12:26:09 2016 +0200
+++ b/src/HOL/Tools/Sledgehammer/async_manager_legacy.ML Sun Aug 14 12:26:09 2016 +0200
@@ -123,7 +123,7 @@
(Synchronized.timed_access global_state
(SOME o time_limit o #timeout_heap) action
|> these
- |> List.app (unregister (false, "Timed out."));
+ |> List.app (unregister (false, "Timed out"));
print_new_messages ();
(* give threads some time to respond to interrupt *)
OS.Process.sleep min_wait_time)
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML Sun Aug 14 12:26:09 2016 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML Sun Aug 14 12:26:09 2016 +0200
@@ -135,8 +135,8 @@
|> filter_used_facts false used_facts
|> map (fn ((name, _), j) => name ^ "@" ^ string_of_int j)
|> commas
- |> enclose ("Fact" ^ plural_s (length facts) ^ " in " ^ quote name ^
- " proof (of " ^ string_of_int (length facts) ^ "): ") "."
+ |> curry (op ^) ("Fact" ^ plural_s (length facts) ^ " in " ^ quote name ^
+ " proof (of " ^ string_of_int (length facts) ^ "): ")
|> writeln
fun spying_str_of_res ({outcome = NONE, used_facts, used_from, ...} : prover_result) =
@@ -206,7 +206,7 @@
not (is_prover_installed ctxt name) then
()
else
- error ("Unexpected outcome: " ^ quote outcome_code ^ ".")
+ error ("Unexpected outcome: " ^ quote outcome_code)
in (outcome_code, message) end
in
if mode = Auto_Try then
@@ -228,11 +228,11 @@
fun string_of_facts facts =
"Including " ^ string_of_int (length facts) ^ " relevant fact" ^ plural_s (length facts) ^ ": " ^
- (facts |> map (fst o fst) |> space_implode " ") ^ "."
+ (facts |> map (fst o fst) |> space_implode " ")
fun string_of_factss factss =
if forall (null o snd) factss then
- "Found no relevant facts."
+ "Found no relevant facts"
else
cat_lines (map (fn (filter, facts) =>
(if filter = "" then "" else quote filter ^ ": ") ^ string_of_facts facts) factss)
@@ -240,7 +240,7 @@
fun run_sledgehammer (params as {verbose, spy, provers, max_facts, ...}) mode writeln_result i
(fact_override as {only, ...}) state =
if null provers then
- error "No prover is set."
+ error "No prover is set"
else
(case subgoal_count state of
0 => (error "No subgoal!"; (false, (noneN, [])))
@@ -269,7 +269,7 @@
nearly_all_facts ctxt ho_atp fact_override keywords css chained hyp_ts concl_t
val _ =
(case find_first (not o is_prover_supported ctxt) provers of
- SOME name => error ("No such prover: " ^ name ^ ".")
+ SOME name => error ("No such prover: " ^ name)
| NONE => ())
val _ = print "Sledgehammering..."
val _ = spying spy (fn () => (state, i, "***", "Starting " ^ str_of_mode mode ^ " mode"))
@@ -319,7 +319,7 @@
in
launch_provers ()
handle Timeout.TIMEOUT _ =>
- (print "Sledgehammer ran out of time."; (unknownN, []))
+ (print "Sledgehammer ran out of time"; (unknownN, []))
end
|> `(fn (outcome_code, _) => outcome_code = someN))
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML Sun Aug 14 12:26:09 2016 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML Sun Aug 14 12:26:09 2016 +0200
@@ -112,7 +112,7 @@
if value <> ["false"] then
param'
else
- error ("Parameter " ^ quote name ^ " cannot be set to \"false\" (cf. " ^ quote name' ^ ").")
+ error ("Parameter " ^ quote name ^ " cannot be set to \"false\" (cf. " ^ quote name' ^ ")")
| NONE =>
(case AList.lookup (op =) negated_alias_params name of
SOME name' => (name',
@@ -144,9 +144,9 @@
else if is_some (Int.fromString name) then
("max_facts", [name])
else
- error ("Unknown parameter: " ^ quote name ^ ".")
+ error ("Unknown parameter: " ^ quote name)
else
- error ("Unknown parameter: " ^ quote name ^ "."))
+ error ("Unknown parameter: " ^ quote name))
(* Ensures that type encodings such as "mono_native?" and "poly_guards!!" are
read correctly. *)
@@ -218,14 +218,14 @@
| SOME s =>
(case Int.fromString s of
SOME n => n
- | NONE => error ("Parameter " ^ quote name ^ " must be assigned an integer value.")))
+ | NONE => error ("Parameter " ^ quote name ^ " must be assigned an integer value")))
fun lookup_real name =
(case lookup name of
NONE => 0.0
| SOME s =>
(case Real.fromString s of
SOME n => n
- | NONE => error ("Parameter " ^ quote name ^ " must be assigned a real value.")))
+ | NONE => error ("Parameter " ^ quote name ^ " must be assigned a real value")))
fun lookup_real_pair name =
(case lookup name of
NONE => (0.0, 0.0)
@@ -341,7 +341,7 @@
else if subcommand = refresh_tptpN then
refresh_systems_on_tptp ()
else
- error ("Unknown subcommand: " ^ quote subcommand ^ ".")
+ error ("Unknown subcommand: " ^ quote subcommand)
end
fun string_of_raw_param (key, values) =
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Sun Aug 14 12:26:09 2016 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Sun Aug 14 12:26:09 2016 +0200
@@ -454,7 +454,7 @@
SOME s => s
| NONE =>
one_line_proof_text ctxt 0 one_line_params ^
- (if isar_proofs = SOME true then "\nWarning: Isar proof construction failed." else ""))
+ (if isar_proofs = SOME true then "\nWarning: Isar proof construction failed" else ""))
end
fun isar_proof_would_be_a_good_idea smt_proofs (meth, play) =
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Sun Aug 14 12:26:09 2016 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Sun Aug 14 12:26:09 2016 +0200
@@ -149,7 +149,7 @@
| "knn_ext" => SOME MaSh_kNN_Ext
| "none" => NONE
| "" => NONE
- | algorithm => (warning ("Unknown MaSh algorithm: " ^ quote algorithm ^ "."); NONE))
+ | algorithm => (warning ("Unknown MaSh algorithm: " ^ quote algorithm); NONE))
val is_mash_enabled = is_some o mash_algorithm
val the_mash_algorithm = the_default MaSh_NB_kNN o mash_algorithm
@@ -1038,7 +1038,7 @@
if verbose andalso auto_level = 0 then
writeln ("MaSh: " ^ quote prover ^ " on " ^ quote name ^ " with " ^
string_of_int num_isar_deps ^ " + " ^ string_of_int (length facts - num_isar_deps) ^
- " facts.")
+ " facts")
else
();
(case run_prover_for_mash ctxt params prover name facts goal of
@@ -1046,7 +1046,7 @@
(if verbose andalso auto_level = 0 then
let val num_facts = length used_facts in
writeln ("Found proof with " ^ string_of_int num_facts ^ " fact" ^
- plural_s num_facts ^ ".")
+ plural_s num_facts)
end
else
();
@@ -1237,7 +1237,7 @@
|> apply2 (map fact_of_raw_fact)
end
-fun mash_unlearn () = (clear_state (); writeln "Reset MaSh.")
+fun mash_unlearn () = (clear_state (); writeln "Reset MaSh")
fun learn_wrt_access_graph ctxt (name, parents, feats, deps)
(accum as (access_G, (fact_xtab, feat_xtab))) =
@@ -1336,9 +1336,9 @@
in
if no_new_facts andalso not run_prover then
if auto_level < 2 then
- "No new " ^ (if run_prover then "automatic" else "Isar") ^ " proofs to learn." ^
+ "No new " ^ (if run_prover then "automatic" else "Isar") ^ " proofs to learn" ^
(if auto_level = 0 andalso not run_prover then
- "\n\nHint: Try " ^ sendback learn_proverN ^ " to learn from an automatic prover."
+ "\n\nHint: Try " ^ sendback learn_proverN ^ " to learn from an automatic prover"
else
"")
else
@@ -1393,7 +1393,7 @@
let val num_proofs = length learns + length relearns in
writeln ("Learned " ^ string_of_int num_proofs ^ " " ^
(if run_prover then "automatic" else "Isar") ^ " proof" ^
- plural_s num_proofs ^ " in the last " ^ string_of_time commit_timeout ^ ".")
+ plural_s num_proofs ^ " in the last " ^ string_of_time commit_timeout)
end
else
())
@@ -1483,7 +1483,7 @@
"Learned " ^ string_of_int num_new_facts ^ " fact" ^ plural_s num_new_facts ^ " and " ^
string_of_int num_nontrivial ^ " nontrivial " ^
(if run_prover then "automatic and " else "") ^ "Isar proof" ^ plural_s num_nontrivial ^
- (if verbose then " in " ^ string_of_time (Timer.checkRealTimer timer) else "") ^ "."
+ (if verbose then " in " ^ string_of_time (Timer.checkRealTimer timer) else "")
else
""
end
@@ -1508,8 +1508,8 @@
plural_s num_facts ^ " for automatic proofs (" ^ quote prover ^ " timeout: " ^
string_of_time timeout ^ ").\n\nCollecting Isar proofs first...");
learn 1 false;
- writeln "Now collecting automatic proofs. This may take several hours. You \
- \can safely stop the learning process at any point.";
+ writeln "Now collecting automatic proofs\n\
+ \This may take several hours; you can safely stop the learning process at any point";
learn 0 true)
else
(writeln ("MaShing through " ^ string_of_int num_facts ^ " fact" ^
@@ -1535,7 +1535,7 @@
fun relevant_facts ctxt (params as {verbose, learn, fact_filter, timeout, ...}) prover
max_facts ({add, only, ...} : fact_override) hyp_ts concl_t facts =
if not (subset (op =) (the_list fact_filter, fact_filters)) then
- error ("Unknown fact filter: " ^ quote (the fact_filter) ^ ".")
+ error ("Unknown fact filter: " ^ quote (the fact_filter))
else if only then
[("", map fact_of_raw_fact facts)]
else if max_facts <= 0 orelse null facts then
@@ -1551,7 +1551,7 @@
(if verbose then
writeln ("Started MaShing through " ^
(if exact then "" else "at least ") ^ string_of_int min_num_facts_to_learn ^
- " fact" ^ plural_s min_num_facts_to_learn ^ " in the background.")
+ " fact" ^ plural_s min_num_facts_to_learn ^ " in the background")
else
());
launch_thread timeout
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML Sun Aug 14 12:26:09 2016 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML Sun Aug 14 12:26:09 2016 +0200
@@ -181,7 +181,7 @@
fun try_command_line banner play command =
let val s = string_of_play_outcome play in
banner ^ ": " ^ Active.sendback_markup_command command ^
- (s |> s <> "" ? enclose " (" ")") ^ "."
+ (s |> s <> "" ? enclose " (" ")")
end
fun one_line_proof_text ctxt num_chained
@@ -189,7 +189,7 @@
let val (chained, extra) = List.partition (fn (_, (sc, _)) => sc = Chained) used_facts in
map fst extra
|> proof_method_command ctxt meth subgoal subgoal_count (map fst chained) num_chained
- |> (if play = Play_Failed then enclose "One-line proof reconstruction failed: " "."
+ |> (if play = Play_Failed then prefix "One-line proof reconstruction failed: "
else try_command_line banner play)
end
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML Sun Aug 14 12:26:09 2016 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML Sun Aug 14 12:26:09 2016 +0200
@@ -194,7 +194,7 @@
sort_strings (supported_atps thy) @ sort_strings (SMT_Config.available_solvers_of ctxt)
|> List.partition (String.isPrefix remote_prefix)
in
- writeln ("Supported provers: " ^ commas (local_provers @ remote_provers) ^ ".")
+ writeln ("Supported provers: " ^ commas (local_provers @ remote_provers))
end
end;
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML Sun Aug 14 12:26:09 2016 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML Sun Aug 14 12:26:09 2016 +0200
@@ -161,7 +161,7 @@
else if File.exists (Path.explode dest_dir) then
Path.append (Path.explode dest_dir) problem_file_name
else
- error ("No such directory: " ^ quote dest_dir ^ ".")
+ error ("No such directory: " ^ quote dest_dir)
val exec = exec full_proofs
val command0 =
(case find_first (fn var => getenv var <> "") (fst exec) of
@@ -176,9 +176,9 @@
in
(case find_first File.exists paths of
SOME path => path
- | NONE => error ("Bad executable: " ^ Path.print (hd paths) ^ "."))
+ | NONE => error ("Bad executable: " ^ Path.print (hd paths)))
end
- | NONE => error ("The environment variable " ^ quote (List.last (fst exec)) ^ " is not set."))
+ | NONE => error ("The environment variable " ^ quote (List.last (fst exec)) ^ " is not set"))
fun split_time s =
let
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML Sun Aug 14 12:26:09 2016 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML Sun Aug 14 12:26:09 2016 +0200
@@ -58,14 +58,14 @@
else if is_smt_prover ctxt name then
SMT_Solver.default_max_relevant ctxt name
else
- error ("No such prover: " ^ name ^ ".")
+ error ("No such prover: " ^ name)
end
fun get_prover ctxt mode name =
let val thy = Proof_Context.theory_of ctxt in
if is_atp thy name then run_atp mode name
else if is_smt_prover ctxt name then run_smt_solver mode name
- else error ("No such prover: " ^ name ^ ".")
+ else error ("No such prover: " ^ name)
end
(* wrapper for calling external prover *)
@@ -116,7 +116,7 @@
| NONE =>
"Found proof" ^
(if length used_facts = length facts then "" else " with " ^ n_facts used_facts) ^
- " (" ^ string_of_time run_time ^ ")."));
+ " (" ^ string_of_time run_time ^ ")"));
result
end
@@ -206,7 +206,7 @@
fun test timeout non_chained =
test_facts params silent prover timeout i n state goal (chained @ non_chained)
in
- (print silent (fn () => "Sledgehammer minimizer: " ^ quote prover_name ^ ".");
+ (print silent (fn () => "Sledgehammer minimizer: " ^ quote prover_name);
(case test timeout non_chained of
result as {outcome = NONE, used_facts, run_time, ...} =>
let
@@ -222,14 +222,14 @@
["Minimized to " ^ n_facts (map fst min_facts)] ^
(case length chained of
0 => ""
- | n => " (plus " ^ string_of_int n ^ " chained)") ^ ".");
+ | n => " (plus " ^ string_of_int n ^ " chained)"));
(if learn then do_learn (maps snd min_facts_and_chained) else ());
(SOME min_facts_and_chained, message)
end
| {outcome = SOME TimedOut, ...} =>
(NONE, fn _ =>
"Timeout: You can increase the time limit using the \"timeout\" option (e.g., \
- \timeout = " ^ string_of_int (10 + Time.toMilliseconds timeout div 1000) ^ "\").")
+ \timeout = " ^ string_of_int (10 + Time.toMilliseconds timeout div 1000) ^ "\")")
| {message, ...} => (NONE, (prefix "Prover error: " o message))))
handle ERROR msg => (NONE, fn _ => "Error: " ^ msg)
end
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML Sun Aug 14 12:26:09 2016 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML Sun Aug 14 12:26:09 2016 +0200
@@ -60,7 +60,7 @@
| failure_of_smt_failure (SMT_Failure.Abnormal_Termination code) =
(case AList.lookup (op =) smt_failures code of
SOME failure => failure
- | NONE => UnknownError ("Abnormal termination with exit code " ^ string_of_int code ^ "."))
+ | NONE => UnknownError ("Abnormal termination with exit code " ^ string_of_int code))
| failure_of_smt_failure SMT_Failure.Out_Of_Memory = OutOfResources
| failure_of_smt_failure (SMT_Failure.Other_Failure s) = UnknownError s
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Sun Aug 14 12:26:09 2016 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Sun Aug 14 12:26:09 2016 +0200
@@ -61,7 +61,7 @@
handle Option.Option =>
let val ss = map quote ((option ? cons "smart") ["true", "false"]) in
error ("Parameter " ^ quote name ^ " must be assigned " ^
- space_implode " " (serial_commas "or" ss) ^ ".")
+ space_implode " " (serial_commas "or" ss))
end
val has_junk =
@@ -71,7 +71,7 @@
let val secs = if has_junk s then NONE else Real.fromString s in
if is_none secs orelse the secs < 0.0 then
error ("Parameter " ^ quote name ^ " must be assigned a nonnegative number of seconds \
- \(e.g., \"60\", \"0.5\") or \"none\".")
+ \(e.g., \"60\", \"0.5\") or \"none\"")
else
seconds (the secs)
end