changeset 47785 | d27bb852c430 |
parent 47770 | 53e30966b4b6 |
child 47788 | 44b33c1e702e |
47784:fe43977e434f | 47785:d27bb852c430 |
---|---|
13 ML {* Proofterm.proofs := 0 *} |
13 ML {* Proofterm.proofs := 0 *} |
14 |
14 |
15 declare [[show_consts]] (* for Refute *) |
15 declare [[show_consts]] (* for Refute *) |
16 declare [[smt_oracle]] |
16 declare [[smt_oracle]] |
17 |
17 |
18 (* |
|
19 ML {* ATP_Problem_Import.isabelle_tptp_file 100 "$TPTP/Problems/PUZ/PUZ107^5.p" *} |
|
20 *) |
|
21 |
|
18 end |
22 end |