author | blanchet |
Fri, 02 Oct 2015 21:21:51 +0200 | |
changeset 61314 | 07eb540da4ab |
parent 61313 | 570dae974f64 |
child 61315 | a48388351990 |
--- a/src/HOL/Metis_Examples/Proxies.thy Fri Oct 02 21:16:16 2015 +0200 +++ b/src/HOL/Metis_Examples/Proxies.thy Fri Oct 02 21:21:51 2015 +0200 @@ -14,8 +14,8 @@ imports Type_Encodings begin -sledgehammer_params [prover = spass, blocking, fact_filter = mepo, timeout = 30, - preplay_timeout = 0, dont_minimize] +sledgehammer_params [prover = spass, fact_filter = mepo, timeout = 30, preplay_timeout = 0, + dont_minimize] text {* Extensionality and set constants *}