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