# HG changeset patch
# User blanchet
# Date 1305206959 -7200
# Node ID 887789ed4b492180cf21030b9d7ade19da19287f
# Parent  f42fd9754724ff66767e32bf63225f40c2af3002
tuning

diff -r f42fd9754724 -r 887789ed4b49 src/HOL/Tools/ATP/atp_problem.ML
--- a/src/HOL/Tools/ATP/atp_problem.ML	Thu May 12 15:29:19 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_problem.ML	Thu May 12 15:29:19 2011 +0200
@@ -24,11 +24,12 @@
   type 'a problem = (string * 'a problem_line list) list
 
 (* official TPTP syntax *)
+  val tptp_special_prefix : string
+  val tptp_false : string
+  val tptp_true : string
   val tptp_tff_type_of_types : string
   val tptp_tff_bool_type : string
   val tptp_tff_individual_type : string
-  val tptp_false : string
-  val tptp_true : string
   val timestamp : unit -> string
   val hashw : word * word -> word
   val hashw_string : string * word -> word
@@ -62,11 +63,12 @@
 type 'a problem = (string * 'a problem_line list) list
 
 (* official TPTP syntax *)
+val tptp_special_prefix = "$"
+val tptp_false = "$false"
+val tptp_true = "$true"
 val tptp_tff_type_of_types = "$tType"
 val tptp_tff_bool_type = "$o"
 val tptp_tff_individual_type = "$i"
-val tptp_false = "$false"
-val tptp_true = "$true"
 
 val timestamp = Date.fmt "%Y-%m-%d %H:%M:%S" o Date.fromTimeLocal o Time.now