equal
deleted
inserted
replaced
4 Importing TPTP files into Isabelle/HOL: parsing TPTP formulas and |
4 Importing TPTP files into Isabelle/HOL: parsing TPTP formulas and |
5 interpreting them as HOL terms (i.e. importing types and type-checking the terms) |
5 interpreting them as HOL terms (i.e. importing types and type-checking the terms) |
6 *) |
6 *) |
7 |
7 |
8 theory TPTP_Interpret |
8 theory TPTP_Interpret |
9 imports Main TPTP_Parser |
9 imports Complex_Main TPTP_Parser |
10 keywords "import_tptp" :: thy_decl |
10 keywords "import_tptp" :: thy_decl |
11 begin |
11 begin |
12 |
12 |
13 typedecl "ind" |
13 typedecl ind |
14 |
14 |
15 ML_file "TPTP_Parser/tptp_interpret.ML" |
15 ML_file "TPTP_Parser/tptp_interpret.ML" |
16 |
16 |
17 end |
17 end |