# HG changeset patch # User blanchet # Date 1306224060 -7200 # Node ID 13cb8895f53815b2a8a8a4830162561de8d44e27 # Parent 4e2d6c1e5392f9ab6e00dba2a652e0cddd057897 tuning diff -r 4e2d6c1e5392 -r 13cb8895f538 src/HOL/Tools/ATP/atp_problem.ML --- 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