# HG changeset patch
# User paulson
# Date 857141072 -3600
# Node ID b7c86d3c9d0a2c0dd441f15c76944843120cbffe
# Parent  351c45bb338dca2e32b1c4814a0f4a14d4b0f056
Addition of de Bruijn formulae

diff -r 351c45bb338d -r b7c86d3c9d0a src/FOL/ex/int.ML
--- a/src/FOL/ex/int.ML	Thu Feb 27 13:44:55 1997 +0100
+++ b/src/FOL/ex/int.ML	Fri Feb 28 15:44:32 1997 +0100
@@ -80,6 +80,26 @@
 getgoal 1;  
 
 
+writeln"de Bruijn formulae";
+
+(*de Bruijn formula with three predicates*)
+goal IFOL.thy "((P<->Q) --> P&Q&R) &    \
+\              ((Q<->R) --> P&Q&R) &    \
+\              ((R<->P) --> P&Q&R) --> P&Q&R";
+by (IntPr.fast_tac 1);
+result();
+
+
+(*de Bruijn formula with five predicates*)
+goal IFOL.thy "((P<->Q) --> P&Q&R&S&T) &    \
+\              ((Q<->R) --> P&Q&R&S&T) &    \
+\              ((R<->S) --> P&Q&R&S&T) &    \
+\              ((S<->T) --> P&Q&R&S&T) &    \
+\              ((T<->P) --> P&Q&R&S&T) --> P&Q&R&S&T";
+by (IntPr.fast_tac 1);
+result();
+
+
 writeln"Intuitionistic FOL: propositional problems based on Pelletier.";
 
 writeln"Problem ~~1";