# HG changeset patch
# User paulson
# Date 928830312 -7200
# Node ID 95abcc002a21992779be6e05fe877adc6bd60271
# Parent  f6bc583a5776c7fa6612174b5d2dd017042a33f7
new classical example from Lewis Carroll via S G Pulman

diff -r f6bc583a5776 -r 95abcc002a21 src/FOL/ex/cla.ML
--- a/src/FOL/ex/cla.ML	Mon Jun 07 22:18:26 1999 +0200
+++ b/src/FOL/ex/cla.ML	Tue Jun 08 10:25:12 1999 +0200
@@ -571,6 +571,18 @@
 by (Blast_tac 1);
 result();
 
+(*Attributed to Lewis Carroll by S. G. Pulman.  The first or last assumption
+can be deleted.*)
+Goal "(ALL x. honest(x) & industrious(x) --> healthy(x)) & \
+\     ~ (EX x. grocer(x) & healthy(x)) & \
+\     (ALL x. industrious(x) & grocer(x) --> honest(x)) & \
+\     (ALL x. cyclist(x) --> industrious(x)) & \
+\     (ALL x. ~healthy(x) & cyclist(x) --> ~honest(x))  \
+\     --> (ALL x. grocer(x) --> ~cyclist(x))";
+by (Blast_tac 1);
+result();
+
+
 writeln"Reached end of file.";
 
 (*Thu Jul 23 1992: loaded in 467s using iffE [on SPARC2] *)
diff -r f6bc583a5776 -r 95abcc002a21 src/HOL/ex/cla.ML
--- a/src/HOL/ex/cla.ML	Mon Jun 07 22:18:26 1999 +0200
+++ b/src/HOL/ex/cla.ML	Tue Jun 08 10:25:12 1999 +0200
@@ -477,6 +477,17 @@
 by (Fast_tac 1);
 result();
 
+(*Attributed to Lewis Carroll by S. G. Pulman.  The first or last assumption
+can be deleted.*)
+Goal "(ALL x. honest(x) & industrious(x) --> healthy(x)) & \
+\     ~ (EX x. grocer(x) & healthy(x)) & \
+\     (ALL x. industrious(x) & grocer(x) --> honest(x)) & \
+\     (ALL x. cyclist(x) --> industrious(x)) & \
+\     (ALL x. ~healthy(x) & cyclist(x) --> ~honest(x))  \
+\     --> (ALL x. grocer(x) --> ~cyclist(x))";
+by (Blast_tac 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) &        \