src/HOL/TPTP/TPTP_Parser/README

+The TPTP parser is generated using ML-Yacc and relies on the ML-Yacc
+library to function. The ML-Yacc library is an external piece of
+software that needs a small modification for use in Isabelle.  The
+file "make_tptp_parser" patches the ML-Yacc library, generates the
+TPTP parser, and patches that to conform to Isabelle's naming
+conventions.
+
+In order to generate the parser from its lex/yacc definition you need
+to have the ML-Yacc binaries. The sources can be downloaded via SVN as
+follows:
+
+ svn co --username anonsvn \
+ https://smlnj-gforge.cs.uchicago.edu/svn/smlnj/ml-yacc/trunk ml-yacc
+
+ML-Yacc is usually distributed with Standard ML of New Jersey, and its
+binaries can also be obtained as packages for some distributions of
+Linux.
+
+The generated parser needs ML-Yacc's library. This is distributed with
+ML-Yacc's source code, in the lib/ directory.
+
+Assuming that you've got the ml-lex and ml-yacc binaries, and have a
+copy of the ML-Yacc sources in this directory, then running
+"make_tptp_parser" will generate two files:
+
+ ml_yacc_lib.ML -- this is a compilation of slightly modified files
+                   making up ML-Yacc's library.
+
+ tptp_lexyacc.ML -- this is a compilation of the SML files making up
+                    the TPTP parser.
+
+Nik Sultana
+8th March 2012