speed-up
authorpaulson
Mon, 01 Dec 1997 12:50:04 +0100
changeset 4330 a5a82aaf2d76
parent 4329 9d99bfdd7441
child 4331 34bb65b037dd
speed-up
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";