author | haftmann |
Fri, 20 Oct 2017 20:57:55 +0200 | |
changeset 66888 | 930abfdf8727 |
parent 62390 | 842917225d56 |
child 69605 | a96320074298 |
permissions | -rw-r--r-- |
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 | 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 | 11 |
begin |
12 |
||
57796 | 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 | 15 |
ML_file "TPTP_Parser/tptp_interpret.ML" |
48891 | 16 |
|
62390 | 17 |
end |