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";