# HG changeset patch
# User paulson
# Date 881142433 -3600
# Node ID c7f6b4256964c2439708cc7c403ef2fd841ba1ff
# Parent  d683b7898c6186ead7f0476ba560a63a9f044f63
updated for latest Blast_tac, which fixes an equality bug

diff -r d683b7898c61 -r c7f6b4256964 src/FOL/ex/cla.ML
--- a/src/FOL/ex/cla.ML	Wed Dec 03 10:45:42 1997 +0100
+++ b/src/FOL/ex/cla.ML	Wed Dec 03 10:47:13 1997 +0100
@@ -402,7 +402,7 @@
 by (assume_tac 1);
 by (res_inst_tac [("x","b")] allE 1);
 by (assume_tac 1);
-by (Blast_tac 1);
+by (Fast_tac 1);    (*Blast_tac's treatment of equality can't do it*)
 result();
 
 writeln"Problem 50";  
@@ -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 (Fast_tac 1);	(*nearly 10 times faster than Blast_tac*)
+by (Blast_tac 1);
 result();
 
 writeln"Problem 55";
@@ -571,4 +571,5 @@
 (*Thu Apr  3 1997: loaded in 44s (on pochard)--using mostly Blast_tac*)
 (*Thu Apr  3 1997: loaded in 96s (on pochard)--addition of two Halting Probs*)
 (*Thu Apr  3 1997: loaded in 98s (on pochard)--using lim-1 for all haz rules*)
+(*Tue Dec  2 1997: loaded in 107s (on pochard)--added 46; new equalSubst*)