isabelle: src/HOL/TPTP/TPTP_Interpret.thy@1c50ddcf6a01 (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
69605 a96320074298 isabelle update -u path_cartouches; wenzelm parents: 62390 diff changeset	15	ML_file \<open>TPTP_Parser/tptp_interpret.ML\<close>
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	nipkow
	Thu, 09 Dec 2021 08:32:29 +0100
changeset 74888	1c50ddcf6a01
parent 69605	a96320074298
permissions	-rw-r--r--