equal
deleted
inserted
replaced
10 |
10 |
11 theory Type_Encodings |
11 theory Type_Encodings |
12 imports Main |
12 imports Main |
13 begin |
13 begin |
14 |
14 |
15 declare [[metis_new_skolemizer]] |
15 declare [[metis_new_skolem]] |
16 |
16 |
17 sledgehammer_params [prover = spass, blocking, fact_filter = mepo, 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 *} |