src/FOL/ex/cla.ML
changeset 2614 0b1364481214
parent 2601 b301958c465d
child 2715 79c35a051196
equal deleted inserted replaced
2613:cc4eb23d37b3 2614:0b1364481214
   516 \                 ((c(Y) & h3(W, Y, Y)) & o(W, b) --> h2(V, Y) & o(V, b))))) \
   516 \                 ((c(Y) & h3(W, Y, Y)) & o(W, b) --> h2(V, Y) & o(V, b))))) \
   517 \  -->                  \
   517 \  -->                  \
   518 \  ~ (EX X. a(X) & (ALL Y. c(Y) --> (ALL Z. d(X, Y, Z))))";
   518 \  ~ (EX X. a(X) & (ALL Y. c(Y) --> (ALL Z. d(X, Y, Z))))";
   519 
   519 
   520 
   520 
       
   521 (* Challenge found on info-hol *)
       
   522 goal FOL.thy
       
   523     "ALL x. EX v w. ALL y z. P(x) & Q(y) --> (P(v) | R(w)) & (R(z) --> Q(v))";
       
   524 by (Deepen_tac 0 1);
       
   525 result();
       
   526 
   521 writeln"Reached end of file.";
   527 writeln"Reached end of file.";
   522 
   528 
   523 (*Thu Jul 23 1992: loaded in 467s using iffE [on SPARC2] *)
   529 (*Thu Jul 23 1992: loaded in 467s using iffE [on SPARC2] *)
   524 (*Mon Nov 14 1994: loaded in 144s [on SPARC10, with deepen_tac] *)
   530 (*Mon Nov 14 1994: loaded in 144s [on SPARC10, with deepen_tac] *)
   525 (*Wed Nov 16 1994: loaded in 138s [after addition of norm_term_skip] *)
   531 (*Wed Nov 16 1994: loaded in 138s [after addition of norm_term_skip] *)