Added P&P&Q <-> P&Q and P|P|Q <-> P|Q
authornipkow
Tue Mar 18 08:43:26 1997 +0100 (1997-03-18 ago)
changeset 280156948cb1a1f9
parent 2800 9741c4c6b62b
child 2802 f119c3686782
Added P&P&Q <-> P&Q and P|P|Q <-> P|Q
src/FOL/simpdata.ML
     1.1 --- a/src/FOL/simpdata.ML	Tue Mar 18 08:42:18 1997 +0100
     1.2 +++ b/src/FOL/simpdata.ML	Tue Mar 18 08:43:26 1997 +0100
     1.3 @@ -17,14 +17,14 @@
     1.4  val conj_simps = map int_prove_fun
     1.5   ["P & True <-> P",      "True & P <-> P",
     1.6    "P & False <-> False", "False & P <-> False",
     1.7 -  "P & P <-> P",
     1.8 +  "P & P <-> P", "P & P & Q <-> P & Q",
     1.9    "P & ~P <-> False",    "~P & P <-> False",
    1.10    "(P & Q) & R <-> P & (Q & R)"];
    1.11  
    1.12  val disj_simps = map int_prove_fun
    1.13   ["P | True <-> True",  "True | P <-> True",
    1.14    "P | False <-> P",    "False | P <-> P",
    1.15 -  "P | P <-> P",
    1.16 +  "P | P <-> P", "P | P | Q <-> P | Q",
    1.17    "(P | Q) | R <-> P | (Q | R)"];
    1.18  
    1.19  val not_simps = map int_prove_fun