# HG changeset patch
# User paulson
# Date 882789697 -3600
# Node ID 76769b48bd88fbec05b389f89d61ef209d527cea
# Parent  fefe21f761d79d1792016787da81ba79e9981421
New example

diff -r fefe21f761d7 -r 76769b48bd88 src/HOL/ex/cla.ML
--- a/src/HOL/ex/cla.ML	Mon Dec 22 11:16:47 1997 +0100
+++ b/src/HOL/ex/cla.ML	Mon Dec 22 12:21:37 1997 +0100
@@ -464,13 +464,21 @@
 by (Blast_tac 1);
 result();
 
+(*From Davis, Obvious Logical Inferences, IJCAI-81, 530-531
+  Fast_tac indeed copes!*)
+goal Prod.thy "(ALL x. F(x) & ~G(x) --> (EX y. H(x,y) & J(y))) & \
+\             (EX x. K(x) & F(x) & (ALL y. H(x,y) --> K(y))) &   \
+\             (ALL x. K(x) --> ~G(x))  -->  (EX x. K(x) & J(x))";
+by (Fast_tac 1);
+result();
+
 (*From Rudnicki, Obvious Inferences, JAR 3 (1987), 383-393.  
   It does seem obvious!*)
 goal Prod.thy
     "(ALL x. F(x) & ~G(x) --> (EX y. H(x,y) & J(y))) &        \
 \    (EX x. K(x) & F(x) & (ALL y. H(x,y) --> K(y)))  &        \
 \    (ALL x. K(x) --> ~G(x))   -->   (EX x. K(x) --> ~G(x))";
-by (Blast_tac 1);
+by (Fast_tac 1);
 result();
 
 goal Prod.thy