--- a/src/HOL/Tools/ATP/atp_proof.ML Sun Jun 19 22:53:15 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_proof.ML Sun Jun 19 22:53:37 2011 +0200
@@ -129,8 +129,8 @@
| string_for_failure (UnsoundProof (true, ss)) =
"The prover found a type-unsound proof " ^ involving ss ^
"even though a supposedly type-sound encoding was used (or, less likely, \
- \your axioms are inconsistent). You might want to report this to the \
- \Isabelle developers."
+ \your axioms are inconsistent). Please report this to the Isabelle \
+ \developers."
| string_for_failure CantConnect = "Cannot connect to remote server."
| string_for_failure TimedOut = "Timed out."
| string_for_failure Inappropriate =
--- a/src/HOL/Tools/ATP/atp_systems.ML Sun Jun 19 22:53:15 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML Sun Jun 19 22:53:37 2011 +0200
@@ -213,11 +213,10 @@
(ProofMissing, "SZS status Theorem"),
(TimedOut, "Failure: Resource limit exceeded (time)"),
(TimedOut, "time limit exceeded"),
- (OutOfResources,
- "# Cannot determine problem status within resource limit"),
+ (OutOfResources, "# Cannot determine problem status"),
(OutOfResources, "SZS status: ResourceOut"),
(OutOfResources, "SZS status ResourceOut")],
- conj_sym_kind = Conjecture, (* FIXME: try out Hypothesis *)
+ conj_sym_kind = Hypothesis,
prem_kind = Conjecture,
formats = [FOF],
best_slices = fn ctxt =>
@@ -257,7 +256,7 @@
(MalformedInput, "Free Variable"),
(SpassTooOld, "tptp2dfg"),
(InternalError, "Please report this error")],
- conj_sym_kind = Axiom, (* FIXME: try out Hypothesis *)
+ conj_sym_kind = Hypothesis,
prem_kind = Conjecture,
formats = [FOF],
best_slices = fn ctxt =>
@@ -299,7 +298,7 @@
(Unprovable, "Termination reason: Satisfiable"),
(VampireTooOld, "not a valid option"),
(Interrupted, "Aborted by signal SIGINT")],
- conj_sym_kind = Conjecture, (* FIXME: try out Hypothesis *)
+ conj_sym_kind = Conjecture,
prem_kind = Conjecture,
formats = [FOF],
best_slices = fn ctxt =>
--- a/src/HOL/ex/ATP_Export.thy Sun Jun 19 22:53:15 2011 +0200
+++ b/src/HOL/ex/ATP_Export.thy Sun Jun 19 22:53:37 2011 +0200
@@ -4,7 +4,7 @@
begin
ML {*
-val do_it = false; (* switch to "true" to generate files *)
+val do_it = false; (* switch to "true" to generate the files *)
val thy = @{theory Complex_Main};
val ctxt = @{context}
*}
--- a/src/HOL/ex/atp_export.ML Sun Jun 19 22:53:15 2011 +0200
+++ b/src/HOL/ex/atp_export.ML Sun Jun 19 22:53:37 2011 +0200
@@ -8,6 +8,7 @@
signature ATP_EXPORT =
sig
+ val theorems_mentioned_in_proof_term : thm -> string list
val generate_tptp_graph_file_for_theory :
Proof.context -> theory -> string -> unit
val generate_tptp_inference_file_for_theory :
@@ -25,16 +26,22 @@
Sledgehammer_Filter.all_facts (Proof_Context.init_global thy) Symtab.empty
true [] []
+(* FIXME: Similar yet different code in "mirabelle.ML". The code here has a few
+ fixes that seem to be missing over there; or maybe the two code portions are
+ not doing the same? *)
fun fold_body_thms f =
let
- fun app n (PBody {thms, ...}) = thms |> fold (fn (i, (name, prop, body)) => fn (x, seen) =>
- if Inttab.defined seen i then (x, seen)
- else
- let
- val body' = Future.join body;
- val (x', seen') = app (n + (if name = "" then 0 else 1)) body' (x, Inttab.update (i, ()) seen);
- in (x' |> n = 1 ? f (name, prop, body'), seen') end);
- in fn bodies => fn x => #1 (fold (app 0) bodies (x, Inttab.empty)) end;
+ fun app n (PBody {thms, ...}) =
+ thms |> fold (fn (i, (name, prop, body)) => fn (x, seen) =>
+ if Inttab.defined seen i then
+ (x, seen)
+ else
+ let
+ val body' = Future.join body
+ val n' = n + (if name = "" then 0 else 1)
+ val (x', seen') = (x, seen) |> n' <= 1 ? app n' body'
+ in (x' |> n = 1 ? f (name, prop, body'), seen') end)
+ in fn bodies => fn x => #1 (fold (app 0) bodies (x, Inttab.empty)) end
fun theorems_mentioned_in_proof_term thm =
let