src/HOL/TPTP/TPTP_Interpret.thy
author wenzelm
Sun, 05 Oct 2014 22:18:40 +0200
changeset 58550 f65911a725ba
parent 57813 0a84dc31601f
child 62390 842917225d56
permissions -rw-r--r--
more explicit syntax, to avoid misunderstanding of foo-bar as 3 separate arguments;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
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