src/HOL/TPTP/TPTP_Parser_Example.thy
2016-05-26 wenzelm 2016-05-26 isabelle update_cartouches -c -t;
2014-01-19 boehmes 2014-01-19 removed obsolete remote_cvc3 and remote_z3
2013-09-03 sultana 2013-09-03 included axiom formulas (removing a FIXME) in the imported problem; turned tests into asserts; changed problem to one which actually succeeds using z3;
2012-08-22 wenzelm 2012-08-22 prefer ML_file over old uses;
2012-04-27 blanchet 2012-04-27 move file to where it belongs
2012-04-23 sultana 2012-04-23 moved function for testing problem-name parsing; list of TPTP test files not immediately evaluated;
2012-04-18 blanchet 2012-04-18 phase out "$TPTP_PROBLEMS_PATH"; prefer "$TPTP" for consistency with CASC setup
2012-04-18 sultana 2012-04-18 fixed type interpretation; output now excludes parsed term; tuned;
2012-04-17 sultana 2012-04-17 more cleaning of tptp tests;
2012-04-04 sultana 2012-04-04 improved import_tptp to use standard TPTP directory structure; extended the TPTP testing theory to include an example of using the import_tptp command;