# HG changeset patch
# User paulson
# Date 961494796 -7200
# Node ID a893887151c0af8aa60fa4497322661fc11efb2b
# Parent  8ae7a2e5119b737ab9add71c850661a426044d4e
changed the Schubert Steamroller proof

diff -r 8ae7a2e5119b -r a893887151c0 src/HOL/ex/mesontest.ML
--- a/src/HOL/ex/mesontest.ML	Tue Jun 20 11:52:38 2000 +0200
+++ b/src/HOL/ex/mesontest.ML	Tue Jun 20 11:53:16 2000 +0200
@@ -503,7 +503,7 @@
 \     (! x y. P3 x & P5 y --> ~R x y) &       \
 \     (! x. (P4 x|P5 x) --> (? y. Q0 y & R x y))      \
 \     --> (? x y. P0 x & P0 y & (? z. Q1 z & R y z & R x y))";
-by (safe_meson_tac 1);   (*40 secs*)
+by (safe_best_meson_tac 1);     (*MUCH faster than iterative deepening*)
 result();
 
 (*The Los problem?  Circulated by John Harrison*)