equal
deleted
inserted
replaced
12 imports Main |
12 imports Main |
13 begin |
13 begin |
14 |
14 |
15 declare [[metis_new_skolemizer]] |
15 declare [[metis_new_skolemizer]] |
16 |
16 |
17 sledgehammer_params [prover = spass, blocking, timeout = 30, |
17 sledgehammer_params [prover = spass, blocking, fact_filter = mepo, timeout = 30, |
18 preplay_timeout = 0, dont_minimize] |
18 preplay_timeout = 0, dont_minimize] |
19 |
19 |
20 text {* Setup for testing Metis exhaustively *} |
20 text {* Setup for testing Metis exhaustively *} |
21 |
21 |
22 lemma fork: "P \<Longrightarrow> P \<Longrightarrow> P" by assumption |
22 lemma fork: "P \<Longrightarrow> P \<Longrightarrow> P" by assumption |