src/HOL/TPTP/TPTP_Parser.thy

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/TPTP/TPTP_Parser.thy	Fri Mar 09 15:38:55 2012 +0000
@@ -0,0 +1,51 @@
+(*  Title:      HOL/TPTP/TPTP_Parser.thy
+    Author:     Nik Sultana, Cambridge University Computer Laboratory
+
+Importing TPTP files into Isabelle/HOL:
+* parsing TPTP formulas;
+* interpreting TPTP formulas as HOL terms (i.e. importing types, and
+    type-checking the terms);
+*)
+
+theory TPTP_Parser
+imports Main
+uses
+  "TPTP_Parser/ml_yacc_lib.ML" (*generated from ML-Yacc's lib*)
+
+  "TPTP_Parser/tptp_syntax.ML"
+  "TPTP_Parser/tptp_lexyacc.ML" (*generated from tptp.lex and tptp.yacc*)
+  "TPTP_Parser/tptp_parser.ML"
+  "TPTP_Parser/tptp_problem_name.ML"
+  "TPTP_Parser/tptp_interpret.ML"
+
+begin
+
+text {*The TPTP parser was generated using ML-Yacc, and needs the
+ML-Yacc library to operate.  This library is included with the parser,
+and we include the next section in accordance with ML-Yacc's terms of
+use.*}
+
+section "ML-YACC COPYRIGHT NOTICE, LICENSE AND DISCLAIMER."
+text {*
+Copyright 1989, 1990 by David R. Tarditi Jr. and Andrew W. Appel
+
+Permission to use, copy, modify, and distribute this software and its
+documentation for any purpose and without fee is hereby granted,
+provided that the above copyright notice appear in all copies and that
+both the copyright notice and this permission notice and warranty
+disclaimer appear in supporting documentation, and that the names of
+David R. Tarditi Jr. and Andrew W. Appel not be used in advertising or
+publicity pertaining to distribution of the software without specific,
+written prior permission.
+
+David R. Tarditi Jr. and Andrew W. Appel disclaim all warranties with
+regard to this software, including all implied warranties of
+merchantability and fitness.  In no event shall David R. Tarditi
+Jr. and Andrew W. Appel be liable for any special, indirect or
+consequential damages or any damages whatsoever resulting from loss of
+use, data or profits, whether in an action of contract, negligence or
+other tortious action, arising out of or in connection with the use or
+performance of this software.
+*}
+
+end
\ No newline at end of file