isabelle: src/HOL/TPTP/TPTP_Interpret.thy@b1d955791529 (annotated)

47509 6f215c2ebd72 split TPTP_Parser thy -- parser can rely on smaller image, whereas TPTP_Interpret requires HOL; sultana parents: diff changeset	1	(* Title: HOL/TPTP/TPTP_Interpret.thy
6f215c2ebd72 split TPTP_Parser thy -- parser can rely on smaller image, whereas TPTP_Interpret requires HOL; sultana parents: diff changeset	2	Author: Nik Sultana, Cambridge University Computer Laboratory
6f215c2ebd72 split TPTP_Parser thy -- parser can rely on smaller image, whereas TPTP_Interpret requires HOL; sultana parents: diff changeset	3
6f215c2ebd72 split TPTP_Parser thy -- parser can rely on smaller image, whereas TPTP_Interpret requires HOL; sultana parents: diff changeset	4	Importing TPTP files into Isabelle/HOL: parsing TPTP formulas and
6f215c2ebd72 split TPTP_Parser thy -- parser can rely on smaller image, whereas TPTP_Interpret requires HOL; sultana parents: diff changeset	5	interpreting them as HOL terms (i.e. importing types and type-checking the terms)
6f215c2ebd72 split TPTP_Parser thy -- parser can rely on smaller image, whereas TPTP_Interpret requires HOL; sultana parents: diff changeset	6	*)
6f215c2ebd72 split TPTP_Parser thy -- parser can rely on smaller image, whereas TPTP_Interpret requires HOL; sultana parents: diff changeset	7
6f215c2ebd72 split TPTP_Parser thy -- parser can rely on smaller image, whereas TPTP_Interpret requires HOL; sultana parents: diff changeset	8	theory TPTP_Interpret
6f215c2ebd72 split TPTP_Parser thy -- parser can rely on smaller image, whereas TPTP_Interpret requires HOL; sultana parents: diff changeset	9	imports Main TPTP_Parser
6f215c2ebd72 split TPTP_Parser thy -- parser can rely on smaller image, whereas TPTP_Interpret requires HOL; sultana parents: diff changeset	10	keywords "import_tptp" :: thy_decl
48891 c0eafbd55de3 prefer ML_file over old uses; wenzelm parents: 47519 diff changeset	11	begin
c0eafbd55de3 prefer ML_file over old uses; wenzelm parents: 47519 diff changeset	12
c0eafbd55de3 prefer ML_file over old uses; wenzelm parents: 47519 diff changeset	13	typedecl "ind"
47509 6f215c2ebd72 split TPTP_Parser thy -- parser can rely on smaller image, whereas TPTP_Interpret requires HOL; sultana parents: diff changeset	14
48891 c0eafbd55de3 prefer ML_file over old uses; wenzelm parents: 47519 diff changeset	15	ML_file "TPTP_Parser/tptp_interpret.ML"
c0eafbd55de3 prefer ML_file over old uses; wenzelm parents: 47519 diff changeset	16
47509 6f215c2ebd72 split TPTP_Parser thy -- parser can rely on smaller image, whereas TPTP_Interpret requires HOL; sultana parents: diff changeset	17	end

author	haftmann
	Fri, 01 Nov 2013 18:51:14 +0100
changeset 54230	b1d955791529
parent 48891	c0eafbd55de3
child 57796	07521fed6071
permissions	-rw-r--r--