# HG changeset patch
# User paulson
# Date 812112595 -3600
# Node ID 6f5d2d76e19b9dee762cae00b71e0643cf2043d6
# Parent  2a2d8c74a756bae85fd3a95e762a2e9dc61328f3
added new example by John Harrison

diff -r 2a2d8c74a756 -r 6f5d2d76e19b src/HOL/ex/mesontest.ML
--- a/src/HOL/ex/mesontest.ML	Thu Sep 21 11:26:44 1995 +0200
+++ b/src/HOL/ex/mesontest.ML	Tue Sep 26 11:49:55 1995 +0100
@@ -213,15 +213,11 @@
 by (safe_meson_tac 1);
 result(); 
 
-writeln"Testing the complete tactic";
-
-(*Not provable by pc_tac: needs multiple instantiation of !.
-  Could be proved trivially by a PROLOG interpreter*)
 goal HOL.thy "(! x. P(x)-->P(f(x)))  &  P(d)-->P(f(f(f(d))))";
 by (safe_meson_tac 1);
 result();
 
-(*Not provable by pc_tac: needs double instantiation of EXISTS*)
+(*Needs double instantiation of EXISTS*)
 goal HOL.thy "? x. P(x) --> P(a) & P(b)";
 by (safe_meson_tac 1);
 result();
@@ -437,7 +433,16 @@
 by (safe_meson_tac 1); 		(*11 secs*)
 result();
 
-(* Example suggested by Johannes Schumann and credited to Pelletier *)
+(*The Los problem?  Circulated by John Harrison*)
+goal HOL.thy "(! x y z. P x y & P y z --> P x z) &	\
+\      (! x y z. Q x y & Q y z --> Q x z) &	\
+\      (! x y. P x y --> P y x) &	\
+\      (! (x::'a) y. P x y | Q x y)	\
+\      --> (! x y. P x y) | (! x y. Q x y)";
+by (safe_meson_tac 1);
+result();
+
+(*A similar example, suggested by Johannes Schumann and credited to Pelletier*)
 goal HOL.thy "(!x y z. P x y --> P y z --> P x z) --> \
 \	(!x y z. Q x y --> Q y z --> Q x z) --> \
 \	(!x y.Q x y --> Q y x) -->  (!x y. P x y | Q x y) --> \