changeset 53989 | 729700091556 |
parent 51929 | 5e8a0b8bb070 |
child 55465 | 0d31c0546286 |
--- a/src/HOL/Metis_Examples/Type_Encodings.thy Sun Sep 29 18:51:01 2013 +0200 +++ b/src/HOL/Metis_Examples/Type_Encodings.thy Mon Sep 30 13:59:07 2013 +0200 @@ -14,9 +14,6 @@ declare [[metis_new_skolem]] -sledgehammer_params [prover = spass, blocking, fact_filter = mepo, timeout = 30, - preplay_timeout = 0, dont_minimize] - text {* Setup for testing Metis exhaustively *} lemma fork: "P \<Longrightarrow> P \<Longrightarrow> P" by assumption