# HG changeset patch
# User lcp
# Date 748862835 -7200
# Node ID b73f7e42135e90f255da50290824f27b0384c46d
# Parent  f17d542276b6c4e1bf122c7ae32c45c2009b03fe
Added example from Avron: Gentzen-Type Systems, Resolution and Tableaux, JAR 10

diff -r f17d542276b6 -r b73f7e42135e src/FOL/ex/cla.ML
--- a/src/FOL/ex/cla.ML	Fri Sep 24 11:13:55 1993 +0200
+++ b/src/FOL/ex/cla.ML	Fri Sep 24 11:27:15 1993 +0200
@@ -139,6 +139,13 @@
 by (fast_tac FOL_cs 1);
 result(); 
 
+(*Discussed in Avron, Gentzen-Type Systems, Resolution and Tableaux,
+  JAR 10 (265-281), 1993.  Proof is trivial!*)
+goal FOL.thy
+    "~ ((EX x.~P(x)) & ((EX x.P(x)) | (EX x.P(x) & Q(x))) & ~ (EX x.P(x)))";
+by (fast_tac FOL_cs 1);
+result();
+
 writeln"Problems requiring quantifier duplication";
 
 (*Needs multiple instantiation of ALL.*)
@@ -202,7 +209,6 @@
 \    ~(EX x.P(x)) --> (EX x.Q(x)) & (ALL x. Q(x)|R(x) --> S(x))  \
 \   --> (EX x. P(x)&R(x))";
 by (fast_tac FOL_cs 1); 
-(*slow*)
 result();
 
 writeln"Problem 25";
@@ -220,7 +226,6 @@
 \     (ALL x. ALL y. p(x) & q(y) --> (r(x) <-> s(y)))	\
 \ --> ((ALL x. p(x)-->r(x)) <-> (ALL x. q(x)-->s(x)))";
 by (fast_tac FOL_cs 1);
-(*slow*)
 result();
 
 writeln"Problem 27";
@@ -230,7 +235,6 @@
 \             ((EX x. R(x) & ~ Q(x)) --> (ALL x. L(x) --> ~ R(x)))  \
 \         --> (ALL x. M(x) --> ~L(x))";
 by (fast_tac FOL_cs 1); 
-(*slow*)
 result();
 
 writeln"Problem 28.  AMENDED";
@@ -239,7 +243,6 @@
 \       ((EX x.S(x)) --> (ALL x. L(x) --> M(x)))  \
 \   --> (ALL x. P(x) & L(x) --> M(x))";
 by (fast_tac FOL_cs 1);  
-(*slow*)
 result();
 
 writeln"Problem 29.  Essentially the same as Principia Mathematica *11.71";