--- a/src/HOL/Tools/ATP/atp_proof.ML Mon May 20 03:41:58 2013 +0200
+++ b/src/HOL/Tools/ATP/atp_proof.ML Mon May 20 11:27:13 2013 +0200
@@ -50,6 +50,7 @@
-> string * failure option
val is_same_atp_step : step_name -> step_name -> bool
val scan_general_id : string list -> string * string list
+ val agsyhol_coreN : string
val satallax_coreN : string
val z3_tptp_coreN : string
val parse_formula :
@@ -468,6 +469,7 @@
>> (fn ((((num, rule), deps), u), names) =>
((num, these names), Unknown, u, rule, map (rpair []) deps))) x
+val agsyhol_coreN = "__agsyhol_core" (* arbitrary *)
val satallax_coreN = "__satallax_core" (* arbitrary *)
val z3_tptp_coreN = "__z3_tptp_core" (* arbitrary *)