src/HOL/TPTP/TPTP_Parser.thy
author paulson <lp15@cam.ac.uk>
Tue Apr 25 16:39:54 2017 +0100 (2017-04-25)
changeset 65578 e4997c181cce
parent 63167 0909deb8059b
child 69605 a96320074298
permissions -rw-r--r--
New material from PNT proof, as well as more default [simp] declarations. Also removed duplicate theorems about geometric series
sultana@46844
     1
(*  Title:      HOL/TPTP/TPTP_Parser.thy
sultana@46844
     2
    Author:     Nik Sultana, Cambridge University Computer Laboratory
sultana@46844
     3
sultana@47509
     4
Parser for TPTP formulas
sultana@46844
     5
*)
sultana@46844
     6
sultana@46844
     7
theory TPTP_Parser
sultana@47509
     8
imports Pure
wenzelm@48891
     9
begin
wenzelm@48891
    10
wenzelm@48891
    11
ML_file "TPTP_Parser/ml_yacc_lib.ML" (*generated from ML-Yacc's lib*)
sultana@46844
    12
wenzelm@48891
    13
ML_file "TPTP_Parser/tptp_syntax.ML"
wenzelm@48891
    14
ML_file "TPTP_Parser/tptp_lexyacc.ML" (*generated from tptp.lex and tptp.yacc*)
wenzelm@48891
    15
ML_file "TPTP_Parser/tptp_parser.ML"
wenzelm@48891
    16
ML_file "TPTP_Parser/tptp_problem_name.ML"
wenzelm@48891
    17
ML_file "TPTP_Parser/tptp_proof.ML"
sultana@46844
    18
wenzelm@63167
    19
text \<open>The TPTP parser was generated using ML-Yacc, and needs the
sultana@46844
    20
ML-Yacc library to operate.  This library is included with the parser,
sultana@46844
    21
and we include the next section in accordance with ML-Yacc's terms of
wenzelm@63167
    22
use.\<close>
sultana@46844
    23
sultana@46844
    24
section "ML-YACC COPYRIGHT NOTICE, LICENSE AND DISCLAIMER."
wenzelm@63167
    25
text \<open>
sultana@46844
    26
Copyright 1989, 1990 by David R. Tarditi Jr. and Andrew W. Appel
sultana@46844
    27
sultana@46844
    28
Permission to use, copy, modify, and distribute this software and its
sultana@46844
    29
documentation for any purpose and without fee is hereby granted,
sultana@46844
    30
provided that the above copyright notice appear in all copies and that
sultana@46844
    31
both the copyright notice and this permission notice and warranty
sultana@46844
    32
disclaimer appear in supporting documentation, and that the names of
sultana@46844
    33
David R. Tarditi Jr. and Andrew W. Appel not be used in advertising or
sultana@46844
    34
publicity pertaining to distribution of the software without specific,
sultana@46844
    35
written prior permission.
sultana@46844
    36
sultana@46844
    37
David R. Tarditi Jr. and Andrew W. Appel disclaim all warranties with
sultana@46844
    38
regard to this software, including all implied warranties of
sultana@46844
    39
merchantability and fitness.  In no event shall David R. Tarditi
sultana@46844
    40
Jr. and Andrew W. Appel be liable for any special, indirect or
sultana@46844
    41
consequential damages or any damages whatsoever resulting from loss of
sultana@46844
    42
use, data or profits, whether in an action of contract, negligence or
sultana@46844
    43
other tortious action, arising out of or in connection with the use or
sultana@46844
    44
performance of this software.
wenzelm@63167
    45
\<close>
sultana@46844
    46
nipkow@62390
    47
end