author | blanchet |
Thu, 07 Aug 2014 12:17:41 +0200 | |
changeset 57813 | 0a84dc31601f |
parent 57810 | 2479dc4ef90b |
child 62390 | 842917225d56 |
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 |
|
47509
6f215c2ebd72
split TPTP_Parser thy -- parser can rely on smaller image, whereas TPTP_Interpret requires HOL;
sultana
parents:
diff
changeset
|
17 |
end |