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