--- a/CONTRIBUTORS Tue Apr 10 06:45:15 2012 +0100
+++ b/CONTRIBUTORS Tue Apr 10 11:42:15 2012 +0200
@@ -6,6 +6,9 @@
Contributions to this Isabelle version
--------------------------------------
+* March 2012: Nik Sultana, University of Cambridge
+ HOL/TPTP parser and import facilities.
+
* January 2012: Florian Haftmann, TUM, et. al.
(Re-)Introduction of the "set" type constructor.
--- a/NEWS Tue Apr 10 06:45:15 2012 +0100
+++ b/NEWS Tue Apr 10 11:42:15 2012 +0200
@@ -456,6 +456,9 @@
* New "eventually_elim" method as a generalized variant of the
eventually_elim* rules. Supports structured proofs.
+* HOL/TPTP: support to parse and import TPTP problems (all languages)
+ into Isabelle/HOL.
+
*** FOL ***