# HG changeset patch
# User lcp
# Date 782729461 -3600
# Node ID ab49d4f96a09862e251b03ce85a56e8bed9c50c5
# Parent  237fce674bfb8934fc8039f3ca04cd16f3a1821a
LK/hardquant/37: deleted call to flexflex_tac: no longer needed

diff -r 237fce674bfb -r ab49d4f96a09 src/LK/ex/hardquant.ML
--- a/src/LK/ex/hardquant.ML	Fri Oct 21 09:47:02 1994 +0100
+++ b/src/LK/ex/hardquant.ML	Fri Oct 21 09:51:01 1994 +0100
@@ -188,17 +188,18 @@
 \       (ALL x z. ~P(x,z) --> (EX y. Q(y,z))) & \
 \       ((EX x y. Q(x,y)) --> (ALL x. R(x,x)))  \
 \   --> (ALL x. EX y. R(x,y))";
-by (pc_tac LK_pack 1);  (*slow*)
-by flexflex_tac;
+by (pc_tac LK_pack 1);
 result();
 
-writeln"Problem 38. NOT PROVED";
+writeln"Problem 38";
 goal LK.thy
  "|- (ALL x. p(a) & (p(x) --> (EX y. p(y) & r(x,y))) -->	\
 \            (EX z. EX w. p(z) & r(x,w) & r(w,z)))  <->		\
 \    (ALL x. (~p(a) | p(x) | (EX z. EX w. p(z) & r(x,w) & r(w,z))) &	\
 \            (~p(a) | ~(EX y. p(y) & r(x,y)) |				\
 \             (EX z. EX w. p(z) & r(x,w) & r(w,z))))";
+by (pc_tac LK_pack 1);
+result();
 
 writeln"Problem 39";
 goal LK.thy "|- ~ (EX x. ALL y. F(y,x) <-> ~F(y,y))";