isabelle: src/HOL/TPTP/TPTP_Interpret.thy@b34fbf33a7ea (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
57796 07521fed6071 correctly interpret arithmetic types blanchet parents: 48891 diff changeset	9	imports Complex_Main TPTP_Parser
47509 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
57796 07521fed6071 correctly interpret arithmetic types blanchet parents: 48891 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
57796 07521fed6071 correctly interpret arithmetic types blanchet parents: 48891 diff changeset	15	ML_file "TPTP_Parser/tptp_interpret.ML"
48891 c0eafbd55de3 prefer ML_file over old uses; wenzelm parents: 47519 diff changeset	16
62390 842917225d56 more canonical names nipkow parents: 57813 diff changeset	17	end

author	wenzelm
	Sat, 04 Nov 2017 12:39:25 +0100
changeset 67001	b34fbf33a7ea
parent 62390	842917225d56
child 69605	a96320074298
permissions	-rw-r--r--