src/FOL/simpdata.ML
changeset 2801 56948cb1a1f9
parent 2727 230f2643107e
child 3206 a3de7f32728c
     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