# HG changeset patch
# User wenzelm
# Date 1334050935 -7200
# Node ID a380515ed7e4c6a6b50816938312274463f03327
# Parent  aac1aa93f1eaa7b137c8bdca21adfad214d75957
some coverage of HOL/TPTP;

diff -r aac1aa93f1ea -r a380515ed7e4 CONTRIBUTORS
--- 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.
 
diff -r aac1aa93f1ea -r a380515ed7e4 NEWS
--- 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 ***