src/HOL/ex/mesontest.ML
changeset 2615 99df9182f5a5
parent 2575 65abf447151b
child 2715 79c35a051196
     1.1 --- a/src/HOL/ex/mesontest.ML	Fri Feb 14 10:36:33 1997 +0100
     1.2 +++ b/src/HOL/ex/mesontest.ML	Fri Feb 14 10:38:48 1997 +0100
     1.3 @@ -508,11 +508,11 @@
     1.4  
     1.5  (*The Los problem?  Circulated by John Harrison*)
     1.6  goal HOL.thy "(! x y z. P x y & P y z --> P x z) &      \
     1.7 -\      (! x y z. Q x y & Q y z --> Q x z) &     \
     1.8 -\      (! x y. P x y --> P y x) &       \
     1.9 -\      (! (x::'a) y. P x y | Q x y)     \
    1.10 +\      (! x y z. Q x y & Q y z --> Q x z) &             \
    1.11 +\      (! x y. P x y --> P y x) &                       \
    1.12 +\      (! x y. P x y | Q x y)                           \
    1.13  \      --> (! x y. P x y) | (! x y. Q x y)";
    1.14 -by (safe_best_meson_tac 1);     (*3 secs; iter. deepening is VERY slow*)
    1.15 +by (safe_best_meson_tac 1);     (*2.3 secs; iter. deepening is VERY slow*)
    1.16  result();
    1.17  
    1.18  (*A similar example, suggested by Johannes Schumann and credited to Pelletier*)