Added a new challenge problem
authorpaulson
Fri Feb 14 10:36:33 1997 +0100 (1997-02-14)
changeset 26140b1364481214
parent 2613 cc4eb23d37b3
child 2615 99df9182f5a5
Added a new challenge problem
src/FOL/ex/cla.ML
     1.1 --- a/src/FOL/ex/cla.ML	Fri Feb 14 10:35:42 1997 +0100
     1.2 +++ b/src/FOL/ex/cla.ML	Fri Feb 14 10:36:33 1997 +0100
     1.3 @@ -518,6 +518,12 @@
     1.4  \  ~ (EX X. a(X) & (ALL Y. c(Y) --> (ALL Z. d(X, Y, Z))))";
     1.5  
     1.6  
     1.7 +(* Challenge found on info-hol *)
     1.8 +goal FOL.thy
     1.9 +    "ALL x. EX v w. ALL y z. P(x) & Q(y) --> (P(v) | R(w)) & (R(z) --> Q(v))";
    1.10 +by (Deepen_tac 0 1);
    1.11 +result();
    1.12 +
    1.13  writeln"Reached end of file.";
    1.14  
    1.15  (*Thu Jul 23 1992: loaded in 467s using iffE [on SPARC2] *)