# HG changeset patch
# User paulson
# Date 880977004 -3600
# Node ID a5a82aaf2d76c4d85046a21b35781b47496d4a21
# Parent  9d99bfdd7441bd4c919dc310958650c922a7e4c8
speed-up

diff -r 9d99bfdd7441 -r a5a82aaf2d76 src/FOL/ex/cla.ML
--- a/src/FOL/ex/cla.ML	Mon Dec 01 08:59:40 1997 +0100
+++ b/src/FOL/ex/cla.ML	Mon Dec 01 12:50:04 1997 +0100
@@ -423,7 +423,7 @@
 goal FOL.thy
     "(EX z w. ALL x y. P(x,y) <->  (x=z & y=w)) -->  \
 \    (EX w. ALL y. EX z. (ALL x. P(x,y) <-> x=z) <-> y=w)";
-by (Blast_tac 1);
+by (Fast_tac 1);	(*nearly 10 times faster than Blast_tac*)
 result();
 
 writeln"Problem 55";