1.1 --- a/src/Doc/Sledgehammer/document/root.tex	Thu Jul 24 00:24:00 2014 +0200
     1.2 +++ b/src/Doc/Sledgehammer/document/root.tex	Thu Jul 24 00:24:00 2014 +0200
     1.3 @@ -201,7 +201,7 @@
     1.4  for Alt-Ergo, set the
     1.5  environment variable \texttt{WHY3\_HOME} to the directory that contains the
     1.6  \texttt{why3} executable.
     1.7 -Sledgehammer has been tested with AgsyHOL 1.0, Alt-Ergo 0.95.2, E 1.0 to 1.8,
     1.8 +Sledgehammer has been tested with AgsyHOL 1.0, Alt-Ergo 0.95.2, E 1.6 to 1.8,
     1.9  LEO-II 1.3.4, Satallax 2.2 to 2.7, SPASS 3.8ds, and Vampire 0.6 to 3.0.%
    1.10  \footnote{Following the rewrite of Vampire, the counter for version numbers was
    1.11  reset to 0; hence the (new) Vampire versions 0.6, 1.0, 1.8, 2.6, and 3.0 are more
    1.12 @@ -837,7 +837,7 @@
    1.13  variable \texttt{E\_HOME} to the directory that contains the \texttt{eproof}
    1.14  executable and \texttt{E\_VERSION} to the version number (e.g., ``1.8''), or
    1.15  install the prebuilt E package from \download. Sledgehammer has been tested with
    1.16 -versions 1.0 to 1.8.
    1.17 +versions 1.6 to 1.8.
    1.18  
    1.19  \item[\labelitemi] \textbf{\textit{e\_males}:} E-MaLeS is a metaprover developed
    1.20  by Daniel K\"uhlwein that implements strategy scheduling on top of E. To use

     2.1 --- a/src/HOL/Tools/ATP/atp_systems.ML	Thu Jul 24 00:24:00 2014 +0200
     2.2 +++ b/src/HOL/Tools/ATP/atp_systems.ML	Thu Jul 24 00:24:00 2014 +0200
     2.3 @@ -212,9 +212,8 @@
     2.4  
     2.5  (* E *)
     2.6  
     2.7 -fun is_e_at_least_1_3 () = string_ord (getenv "E_VERSION", "1.3") <> LESS
     2.8 -fun is_e_at_least_1_6 () = string_ord (getenv "E_VERSION", "1.6") <> LESS
     2.9  fun is_e_at_least_1_8 () = string_ord (getenv "E_VERSION", "1.8") <> LESS
    2.10 +fun is_e_at_least_1_9 () = string_ord (getenv "E_VERSION", "1.9") <> LESS
    2.11  
    2.12  val e_smartN = "smart"
    2.13  val e_autoN = "auto"
    2.14 @@ -286,29 +285,19 @@
    2.15         else "")
    2.16      end
    2.17  
    2.18 -fun effective_e_selection_heuristic ctxt =
    2.19 -  if is_e_at_least_1_3 () then Config.get ctxt e_selection_heuristic
    2.20 -  else e_autoN
    2.21 -
    2.22 -fun e_kbo () = if is_e_at_least_1_3 () then "KBO6" else "KBO"
    2.23 -
    2.24  val e_config : atp_config =
    2.25    {exec = (fn () => (["E_HOME"],
    2.26 -     if is_e_at_least_1_8 () then ["eprover"] else ["eproof_ram", "eproof"])),
    2.27 +     if is_e_at_least_1_9 () then ["eprover"] else ["eproof_ram", "eproof"])),
    2.28     arguments = fn ctxt => fn full_proof => fn heuristic => fn timeout => fn file_name =>
    2.29       fn ({is_lpo, gen_weights, gen_prec, ...}, ord_info, sel_weights) =>
    2.30         (if is_e_at_least_1_8 () then "--auto-schedule " else "") ^
    2.31         "--tstp-in --tstp-out --silent " ^
    2.32         e_selection_weight_arguments ctxt heuristic sel_weights ^ " " ^
    2.33         e_term_order_info_arguments gen_weights gen_prec ord_info ^ " " ^
    2.34 -       "--term-ordering=" ^ (if is_lpo then "LPO4" else e_kbo ()) ^ " " ^
    2.35 +       "--term-ordering=" ^ (if is_lpo then "LPO4" else "KBO6") ^ " " ^
    2.36         "--cpu-limit=" ^ string_of_int (to_secs 2 timeout) ^
    2.37 -       (if is_e_at_least_1_8 () then
    2.38 -          " --proof-object=1"
    2.39 -        else
    2.40 -          " --output-level=5" ^
    2.41 -          (if is_e_at_least_1_6 () then " --pcl-shell-level=" ^ (if full_proof then "0" else "2")
    2.42 -           else "")) ^
    2.43 +       (if is_e_at_least_1_9 () then " --proof-object=3"
    2.44 +        else " --output-level=5 --pcl-shell-level=" ^ (if full_proof then "0" else "2")) ^
    2.45         " " ^ file_name,
    2.46     proof_delims =
    2.47       [("# SZS output start CNFRefutation", "# SZS output end CNFRefutation")] @
    2.48 @@ -319,7 +308,7 @@
    2.49       known_szs_status_failures,
    2.50     prem_role = Conjecture,
    2.51     best_slices = fn ctxt =>
    2.52 -     let val heuristic = effective_e_selection_heuristic ctxt in
    2.53 +     let val heuristic = Config.get ctxt e_selection_heuristic in
    2.54         (* FUDGE *)
    2.55         if heuristic = e_smartN then
    2.56           [(0.15, (((128, meshN), FOF, "mono_tags??", combsN, false), e_fun_weightN)),