equal
deleted
inserted
replaced
6 |
6 |
7 theory ATP_Problem_Import |
7 theory ATP_Problem_Import |
8 imports Complex_Main TPTP_Interpret "HOL-Library.Refute" |
8 imports Complex_Main TPTP_Interpret "HOL-Library.Refute" |
9 begin |
9 begin |
10 |
10 |
11 ML_file "sledgehammer_tactics.ML" |
11 ML_file \<open>sledgehammer_tactics.ML\<close> |
12 |
12 |
13 ML \<open>Proofterm.proofs := 0\<close> |
13 ML \<open>Proofterm.proofs := 0\<close> |
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 declare [[unify_search_bound = 60]] |
18 declare [[unify_search_bound = 60]] |
19 declare [[unify_trace_bound = 60]] |
19 declare [[unify_trace_bound = 60]] |
20 |
20 |
21 ML_file "atp_problem_import.ML" |
21 ML_file \<open>atp_problem_import.ML\<close> |
22 |
22 |
23 (* |
23 (* |
24 ML {* ATP_Problem_Import.isabelle_tptp_file @{theory} 50 "$TPTP/Problems/PUZ/PUZ107^5.p" *} |
24 ML {* ATP_Problem_Import.isabelle_tptp_file @{theory} 50 "$TPTP/Problems/PUZ/PUZ107^5.p" *} |
25 ML {* ATP_Problem_Import.isabelle_hot_tptp_file @{theory} 20 "$TPTP/Problems/SYO/SYO304^5.p" *} |
25 ML {* ATP_Problem_Import.isabelle_hot_tptp_file @{theory} 20 "$TPTP/Problems/SYO/SYO304^5.p" *} |
26 *) |
26 *) |