# HG changeset patch
# User paulson
# Date 830951241 -7200
# Node ID c064cae981d673799d4e338f2f2fd4f38809e838
# Parent  c06d01f75764600b17cf90e6a10c3c7b1081cecb
Two new "obvious" examples

diff -r c06d01f75764 -r c064cae981d6 src/HOL/ex/cla.ML
--- a/src/HOL/ex/cla.ML	Wed May 01 10:43:16 1996 +0200
+++ b/src/HOL/ex/cla.ML	Wed May 01 13:47:21 1996 +0200
@@ -460,4 +460,22 @@
 by (fast_tac HOL_cs 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 (fast_tac HOL_cs 1);
+result();
+
+goal Prod.thy
+    "(ALL x y. R(x,y) | R(y,x)) &                \
+\    (ALL x y. S(x,y) & S(y,x) --> x=y) &        \
+\    (ALL x y. R(x,y) --> S(x,y))    -->   (ALL x y. S(x,y) --> R(x,y))";
+by (fast_tac HOL_cs 1);
+result();
+
+
+
 writeln"Reached end of file.";