# HG changeset patch
# User blanchet
# Date 1330440891 -3600
# Node ID 4a03b30e04cb8243406213659c61c440a8aa6cf8
# Parent  ac701d7f7c3b4d1af0a6b8a9278a1b6a05f97c40
use SPASS instead of E for Metis examples -- it's seems faster for these small problems

diff -r ac701d7f7c3b -r 4a03b30e04cb src/HOL/Metis_Examples/Proxies.thy
--- a/src/HOL/Metis_Examples/Proxies.thy	Tue Feb 28 15:54:51 2012 +0100
+++ b/src/HOL/Metis_Examples/Proxies.thy	Tue Feb 28 15:54:51 2012 +0100
@@ -51,10 +51,9 @@
 by linarith
 
 lemma "B \<le> C"
-sledgehammer [type_enc = poly_args, max_relevant = 100, expect = some]
+sledgehammer [expect = some]
 by (metis_exhaust B_def C_def int_le_0_imp_le_1 predicate1I)
 
-
 text {* Proxies for logical constants *}
 
 lemma "id (op =) x x"
diff -r ac701d7f7c3b -r 4a03b30e04cb src/HOL/Metis_Examples/Type_Encodings.thy
--- a/src/HOL/Metis_Examples/Type_Encodings.thy	Tue Feb 28 15:54:51 2012 +0100
+++ b/src/HOL/Metis_Examples/Type_Encodings.thy	Tue Feb 28 15:54:51 2012 +0100
@@ -14,7 +14,8 @@
 
 declare [[metis_new_skolemizer]]
 
-sledgehammer_params [prover = e, blocking, timeout = 10, preplay_timeout = 0]
+sledgehammer_params [prover = spass, blocking, timeout = 30,
+                     preplay_timeout = 0, dont_minimize]
 
 text {* Setup for testing Metis exhaustively *}