# 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";