author | sultana |
Tue, 10 Apr 2012 06:45:15 +0100 | |
changeset 47411 | 7df9a4f320a5 |
parent 46951 | 4e032ac36134 |
child 47509 | 6f215c2ebd72 |
permissions | -rw-r--r-- |
46844 | 1 |
(* Title: HOL/TPTP/TPTP_Parser.thy |
2 |
Author: Nik Sultana, Cambridge University Computer Laboratory |
|
3 |
||
4 |
Importing TPTP files into Isabelle/HOL: |
|
5 |
* parsing TPTP formulas; |
|
6 |
* interpreting TPTP formulas as HOL terms (i.e. importing types, and |
|
7 |
type-checking the terms); |
|
8 |
*) |
|
9 |
||
10 |
theory TPTP_Parser |
|
11 |
imports Main |
|
46951 | 12 |
keywords "import_tptp" :: thy_decl |
46844 | 13 |
uses |
14 |
"TPTP_Parser/ml_yacc_lib.ML" (*generated from ML-Yacc's lib*) |
|
15 |
||
16 |
"TPTP_Parser/tptp_syntax.ML" |
|
17 |
"TPTP_Parser/tptp_lexyacc.ML" (*generated from tptp.lex and tptp.yacc*) |
|
18 |
"TPTP_Parser/tptp_parser.ML" |
|
19 |
"TPTP_Parser/tptp_problem_name.ML" |
|
47411
7df9a4f320a5
moved non-interpret-specific code to different module
sultana
parents:
46951
diff
changeset
|
20 |
"TPTP_Parser/tptp_proof.ML" |
46844 | 21 |
"TPTP_Parser/tptp_interpret.ML" |
22 |
||
23 |
begin |
|
24 |
||
25 |
text {*The TPTP parser was generated using ML-Yacc, and needs the |
|
26 |
ML-Yacc library to operate. This library is included with the parser, |
|
27 |
and we include the next section in accordance with ML-Yacc's terms of |
|
28 |
use.*} |
|
29 |
||
30 |
section "ML-YACC COPYRIGHT NOTICE, LICENSE AND DISCLAIMER." |
|
31 |
text {* |
|
32 |
Copyright 1989, 1990 by David R. Tarditi Jr. and Andrew W. Appel |
|
33 |
||
34 |
Permission to use, copy, modify, and distribute this software and its |
|
35 |
documentation for any purpose and without fee is hereby granted, |
|
36 |
provided that the above copyright notice appear in all copies and that |
|
37 |
both the copyright notice and this permission notice and warranty |
|
38 |
disclaimer appear in supporting documentation, and that the names of |
|
39 |
David R. Tarditi Jr. and Andrew W. Appel not be used in advertising or |
|
40 |
publicity pertaining to distribution of the software without specific, |
|
41 |
written prior permission. |
|
42 |
||
43 |
David R. Tarditi Jr. and Andrew W. Appel disclaim all warranties with |
|
44 |
regard to this software, including all implied warranties of |
|
45 |
merchantability and fitness. In no event shall David R. Tarditi |
|
46 |
Jr. and Andrew W. Appel be liable for any special, indirect or |
|
47 |
consequential damages or any damages whatsoever resulting from loss of |
|
48 |
use, data or profits, whether in an action of contract, negligence or |
|
49 |
other tortious action, arising out of or in connection with the use or |
|
50 |
performance of this software. |
|
51 |
*} |
|
52 |
||
53 |
end |