author | paulson |
Mon, 01 Dec 1997 12:50:04 +0100 | |
changeset 4330 | a5a82aaf2d76 |
parent 4329 | 9d99bfdd7441 |
child 4331 | 34bb65b037dd |
src/FOL/ex/cla.ML | file | annotate | diff | comparison | revisions |
--- 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";