isabelle: src/HOL/TPTP/TPTP_Interpret.thy@a78612c67ec0 (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
47509 6f215c2ebd72 split TPTP_Parser thy -- parser can rely on smaller image, whereas TPTP_Interpret requires HOL; sultana parents: diff changeset	17	end

author	wenzelm
	Wed, 26 Nov 2014 20:05:34 +0100
changeset 59058	a78612c67ec0
parent 57813	0a84dc31601f
child 62390	842917225d56
permissions	-rw-r--r--