# HG changeset patch
# User blanchet
# Date 1319886958 -7200
# Node ID d8c8c2fcab2cd19d3ca10b51ea089deccb558b6b
# Parent  ee584ff987c328c7bd7c49d9d33a08bf57112a2c
specify proof output level 1 (i.e. no detailed, potentially huge E proofs) to LEO-II; requires version 1.2.9

diff -r ee584ff987c3 -r d8c8c2fcab2c doc-src/Sledgehammer/sledgehammer.tex
--- a/doc-src/Sledgehammer/sledgehammer.tex	Sat Oct 29 13:15:58 2011 +0200
+++ b/doc-src/Sledgehammer/sledgehammer.tex	Sat Oct 29 13:15:58 2011 +0200
@@ -724,7 +724,8 @@
 
 \item[$\bullet$] \textbf{\textit{leo2}:} LEO-II is an automatic
 higher-order prover developed by Christoph Benzm\"uller et al.\ \cite{leo2},
-with support for the TPTP many-typed higher-order syntax (THF0).
+with support for the TPTP many-typed higher-order syntax (THF0). Sledgehammer
+requires version 1.2.9 or above.
 
 \item[$\bullet$] \textbf{\textit{metis}:} Although it is much less powerful than
 the external provers, Metis itself can be used for proof search.
diff -r ee584ff987c3 -r d8c8c2fcab2c src/HOL/Tools/ATP/atp_systems.ML
--- a/src/HOL/Tools/ATP/atp_systems.ML	Sat Oct 29 13:15:58 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Sat Oct 29 13:15:58 2011 +0200
@@ -255,7 +255,7 @@
    required_execs = [],
    arguments =
      fn _ => fn _ => fn sos => fn timeout => fn _ =>
-        "--proofoutput --timeout " ^ string_of_int (to_secs 1 timeout)
+        "--proofoutput 1 --timeout " ^ string_of_int (to_secs 1 timeout)
         |> sos = sosN ? prefix "--sos ",
    proof_delims = tstp_proof_delims,
    known_failures =