--- a/src/HOL/Tools/ATP/atp_problem.ML Tue May 24 10:00:38 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_problem.ML Tue May 24 10:01:00 2011 +0200
@@ -27,13 +27,15 @@
(* official TPTP syntax *)
val tptp_special_prefix : string
+ val tptp_has_type : string
val tptp_type_of_types : string
val tptp_bool_type : string
val tptp_individual_type : string
val tptp_fun_type : string
val tptp_false : string
val tptp_true : string
- val tptp_app_op : string
+ val tptp_not : string
+ val tptp_app : string
val is_atp_variable : string -> bool
val mk_anot : ('a, 'b, 'c) formula -> ('a, 'b, 'c) formula
val mk_aconn :
@@ -77,13 +79,15 @@
(* official TPTP syntax *)
val tptp_special_prefix = "$"
+val tptp_has_type = ":"
val tptp_type_of_types = "$tType"
val tptp_bool_type = "$o"
val tptp_individual_type = "$i"
val tptp_fun_type = ">"
val tptp_false = "$false"
val tptp_true = "$true"
-val tptp_app_op = "@"
+val tptp_not = "~"
+val tptp_app = "@"
fun is_atp_variable s = Char.isUpper (String.sub (s, 0))
@@ -145,7 +149,7 @@
fun string_for_quantifier AForall = "!"
| string_for_quantifier AExists = "?"
-fun string_for_connective ANot = "~"
+fun string_for_connective ANot = tptp_not
| string_for_connective AAnd = "&"
| string_for_connective AOr = "|"
| string_for_connective AImplies = "=>"
@@ -206,8 +210,6 @@
(** CNF UEQ (Waldmeister) **)
-exception LOST_CONJECTURE of unit
-
fun is_problem_line_negated (Formula (_, _, AConn (ANot, _), _, _)) = true
| is_problem_line_negated _ = false