changed the Schubert Steamroller proof
authorpaulson
Tue Jun 20 11:53:16 2000 +0200 (2000-06-20)
changeset 9092a893887151c0
parent 9091 8ae7a2e5119b
child 9093 2e608fa6c404
changed the Schubert Steamroller proof
src/HOL/ex/mesontest.ML
     1.1 --- a/src/HOL/ex/mesontest.ML	Tue Jun 20 11:52:38 2000 +0200
     1.2 +++ b/src/HOL/ex/mesontest.ML	Tue Jun 20 11:53:16 2000 +0200
     1.3 @@ -503,7 +503,7 @@
     1.4  \     (! x y. P3 x & P5 y --> ~R x y) &       \
     1.5  \     (! x. (P4 x|P5 x) --> (? y. Q0 y & R x y))      \
     1.6  \     --> (? x y. P0 x & P0 y & (? z. Q1 z & R y z & R x y))";
     1.7 -by (safe_meson_tac 1);   (*40 secs*)
     1.8 +by (safe_best_meson_tac 1);     (*MUCH faster than iterative deepening*)
     1.9  result();
    1.10  
    1.11  (*The Los problem?  Circulated by John Harrison*)