isabelle: src/HOL/TPTP/TPTP_Interpret.thy@cd8f55c358c5 (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	immler
	Mon, 16 Dec 2013 17:08:22 +0100
changeset 54782	cd8f55c358c5
parent 48891	c0eafbd55de3
child 57796	07521fed6071
permissions	-rw-r--r--