some coverage of HOL/TPTP;
authorwenzelm
Tue Apr 10 11:42:15 2012 +0200 (2012-04-10)
changeset 47413a380515ed7e4
parent 47412 aac1aa93f1ea
child 47414 b2eafae4d401
some coverage of HOL/TPTP;
CONTRIBUTORS
NEWS
     1.1 --- a/CONTRIBUTORS	Tue Apr 10 06:45:15 2012 +0100
     1.2 +++ b/CONTRIBUTORS	Tue Apr 10 11:42:15 2012 +0200
     1.3 @@ -6,6 +6,9 @@
     1.4  Contributions to this Isabelle version
     1.5  --------------------------------------
     1.6  
     1.7 +* March 2012: Nik Sultana, University of Cambridge
     1.8 +  HOL/TPTP parser and import facilities.
     1.9 +
    1.10  * January 2012: Florian Haftmann, TUM, et. al.
    1.11    (Re-)Introduction of the "set" type constructor.
    1.12  
     2.1 --- a/NEWS	Tue Apr 10 06:45:15 2012 +0100
     2.2 +++ b/NEWS	Tue Apr 10 11:42:15 2012 +0200
     2.3 @@ -456,6 +456,9 @@
     2.4  * New "eventually_elim" method as a generalized variant of the
     2.5    eventually_elim* rules. Supports structured proofs.
     2.6  
     2.7 +* HOL/TPTP: support to parse and import TPTP problems (all languages)
     2.8 +  into Isabelle/HOL.
     2.9 +
    2.10  
    2.11  *** FOL ***
    2.12