--- a/src/HOL/Tools/ATP/atp_problem.ML Fri Aug 20 14:18:55 2010 +0200
+++ b/src/HOL/Tools/ATP/atp_problem.ML Fri Aug 20 15:16:27 2010 +0200
@@ -15,7 +15,7 @@
AConn of connective * ('a, 'b) formula list |
AAtom of 'b
- datatype kind = Axiom | Conjecture
+ datatype kind = Axiom | Hypothesis | Conjecture
datatype 'a problem_line = Fof of string * kind * ('a, 'a fo_term) formula
type 'a problem = (string * 'a problem_line list) list
@@ -42,7 +42,7 @@
AConn of connective * ('a, 'b) formula list |
AAtom of 'b
-datatype kind = Axiom | Conjecture
+datatype kind = Axiom | Hypothesis | Conjecture
datatype 'a problem_line = Fof of string * kind * ('a, 'a fo_term) formula
type 'a problem = (string * 'a problem_line list) list
@@ -76,8 +76,11 @@
fun string_for_problem_line (Fof (ident, kind, phi)) =
"fof(" ^ ident ^ ", " ^
- (case kind of Axiom => "axiom" | Conjecture => "conjecture") ^ ",\n" ^
- " (" ^ string_for_formula phi ^ ")).\n"
+ (case kind of
+ Axiom => "axiom"
+ | Hypothesis => "hypothesis"
+ | Conjecture => "conjecture") ^
+ ",\n (" ^ string_for_formula phi ^ ")).\n"
fun strings_for_tptp_problem problem =
"% This file was generated by Isabelle (most likely Sledgehammer)\n\
\% " ^ timestamp () ^ "\n" ::