| changeset 48891 | c0eafbd55de3 |
| parent 47519 | 9c3acd90063a |
| child 57796 | 07521fed6071 |
| 48890:d72ca5742f80 | 48891:c0eafbd55de3 |
|---|---|
6 *) |
6 *) |
7 |
7 |
8 theory TPTP_Interpret |
8 theory TPTP_Interpret |
9 imports Main TPTP_Parser |
9 imports Main TPTP_Parser |
10 keywords "import_tptp" :: thy_decl |
10 keywords "import_tptp" :: thy_decl |
11 uses ("TPTP_Parser/tptp_interpret.ML") |
11 begin |
12 |
12 |
13 begin |
|
14 typedecl "ind" |
13 typedecl "ind" |
15 use "TPTP_Parser/tptp_interpret.ML" |
14 |
15 ML_file "TPTP_Parser/tptp_interpret.ML" |
|
16 |
|
16 end |
17 end |