--- a/src/HOL/TPTP/TPTP_Parser/tptp_proof.ML Wed Feb 19 15:57:02 2014 +0000
+++ b/src/HOL/TPTP/TPTP_Parser/tptp_proof.ML Wed Feb 19 15:57:02 2014 +0000
@@ -113,6 +113,7 @@
(inference_name,
analyse_useful_info useful_info [],
analyse_parent_info parent_info [])))
+
| analyse_annot
(General_Data
(Application
@@ -129,6 +130,17 @@
General_Data (Number (Int_num, defname))])), _) =
(SOME (File (filename, defname)))
+ (*This was added to support Satallax proofs.*)
+ | analyse_annot
+ (General_Data
+ (Application
+ ("introduced",
+ [General_Data (Atomic_Word "assumption"),
+ General_List []])), _) =
+ (SOME (Inference
+ ("assumption", [], [])))
+
+
| analyse_annot (other, _) = raise (ANNOT_STRUCTURE other)
in
case annot of