# HG changeset patch # User blanchet # Date 1306877967 -7200 # Node ID 1286e56edf0654b185db3c2d018137637e2f4277 # Parent e3c7b07704bc0aa37d9d3d78b3835b4bdaea4f29 speed up example by disabling preplay, and temporarily comment out a broken Sledgehammer call diff -r e3c7b07704bc -r 1286e56edf06 src/HOL/Metis_Examples/HO_Reas.thy --- a/src/HOL/Metis_Examples/HO_Reas.thy Tue May 31 19:28:03 2011 +0200 +++ b/src/HOL/Metis_Examples/HO_Reas.thy Tue May 31 23:39:27 2011 +0200 @@ -10,7 +10,7 @@ declare [[metis_new_skolemizer]] -sledgehammer_params [prover = e, blocking, timeout = 10] +sledgehammer_params [prover = e, blocking, timeout = 10, preplay_timeout = 0] text {* Extensionality and set constants *} @@ -48,7 +48,9 @@ by linarith lemma "B \ C" +(* FIXME: sledgehammer [type_sys = poly_args, max_relevant = 200, expect = some] +*) by (metis B_def C_def int_le_0_imp_le_1 predicate1I)