1.1 --- a/src/FOL/ex/int.ML	Thu Feb 27 13:44:55 1997 +0100
     1.2 +++ b/src/FOL/ex/int.ML	Fri Feb 28 15:44:32 1997 +0100
     1.3 @@ -80,6 +80,26 @@
     1.4  getgoal 1;  
     1.5  
     1.6  
     1.7 +writeln"de Bruijn formulae";
     1.8 +
     1.9 +(*de Bruijn formula with three predicates*)
    1.10 +goal IFOL.thy "((P<->Q) --> P&Q&R) &    \
    1.11 +\              ((Q<->R) --> P&Q&R) &    \
    1.12 +\              ((R<->P) --> P&Q&R) --> P&Q&R";
    1.13 +by (IntPr.fast_tac 1);
    1.14 +result();
    1.15 +
    1.16 +
    1.17 +(*de Bruijn formula with five predicates*)
    1.18 +goal IFOL.thy "((P<->Q) --> P&Q&R&S&T) &    \
    1.19 +\              ((Q<->R) --> P&Q&R&S&T) &    \
    1.20 +\              ((R<->S) --> P&Q&R&S&T) &    \
    1.21 +\              ((S<->T) --> P&Q&R&S&T) &    \
    1.22 +\              ((T<->P) --> P&Q&R&S&T) --> P&Q&R&S&T";
    1.23 +by (IntPr.fast_tac 1);
    1.24 +result();
    1.25 +
    1.26 +
    1.27  writeln"Intuitionistic FOL: propositional problems based on Pelletier.";
    1.28  
    1.29  writeln"Problem ~~1";