author | sultana |
Tue, 17 Apr 2012 16:14:07 +0100 | |
changeset 47519 | 9c3acd90063a |
parent 47509 | 6f215c2ebd72 |
child 48891 | c0eafbd55de3 |
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 |
6f215c2ebd72
split TPTP_Parser thy -- parser can rely on smaller image, whereas TPTP_Interpret requires HOL;
sultana
parents:
diff
changeset
|
9 |
imports Main TPTP_Parser |
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 |
47519 | 11 |
uses ("TPTP_Parser/tptp_interpret.ML") |
47509
6f215c2ebd72
split TPTP_Parser thy -- parser can rely on smaller image, whereas TPTP_Interpret requires HOL;
sultana
parents:
diff
changeset
|
12 |
|
6f215c2ebd72
split TPTP_Parser thy -- parser can rely on smaller image, whereas TPTP_Interpret requires HOL;
sultana
parents:
diff
changeset
|
13 |
begin |
47519 | 14 |
typedecl "ind" |
15 |
use "TPTP_Parser/tptp_interpret.ML" |
|
47509
6f215c2ebd72
split TPTP_Parser thy -- parser can rely on smaller image, whereas TPTP_Interpret requires HOL;
sultana
parents:
diff
changeset
|
16 |
end |