| changeset 47714 | d6683fe037b1 |
| parent 47670 | 24babc4b1925 |
| child 47765 | 18f37b7aa6a6 |
| 47713:bd0683000a0f | 47714:d6683fe037b1 |
|---|---|
9 uses ("atp_problem_import.ML") |
9 uses ("atp_problem_import.ML") |
10 begin |
10 begin |
11 |
11 |
12 declare [[show_consts]] (* for Refute *) |
12 declare [[show_consts]] (* for Refute *) |
13 |
13 |
14 typedecl iota (* for TPTP *) |
|
15 |
|
16 use "atp_problem_import.ML" |
14 use "atp_problem_import.ML" |
17 |
15 |
18 end |
16 end |