# HG changeset patch
# User nipkow
# Date 858671006 -3600
# Node ID 56948cb1a1f912a84685e2458e58e0b3b6505371
# Parent  9741c4c6b62b2c193a2eaa7e260fe16982ad4ae4
Added P&P&Q <-> P&Q and P|P|Q <-> P|Q

diff -r 9741c4c6b62b -r 56948cb1a1f9 src/FOL/simpdata.ML
--- a/src/FOL/simpdata.ML	Tue Mar 18 08:42:18 1997 +0100
+++ b/src/FOL/simpdata.ML	Tue Mar 18 08:43:26 1997 +0100
@@ -17,14 +17,14 @@
 val conj_simps = map int_prove_fun
  ["P & True <-> P",      "True & P <-> P",
   "P & False <-> False", "False & P <-> False",
-  "P & P <-> P",
+  "P & P <-> P", "P & P & Q <-> P & Q",
   "P & ~P <-> False",    "~P & P <-> False",
   "(P & Q) & R <-> P & (Q & R)"];
 
 val disj_simps = map int_prove_fun
  ["P | True <-> True",  "True | P <-> True",
   "P | False <-> P",    "False | P <-> P",
-  "P | P <-> P",
+  "P | P <-> P", "P | P | Q <-> P | Q",
   "(P | Q) | R <-> P | (Q | R)"];
 
 val not_simps = map int_prove_fun