src/HOL/Groebner_Basis.thy
changeset 67091 1393c2340eec
parent 64593 50c715579715
child 68100 b2d84b1114fa
     1.1 --- a/src/HOL/Groebner_Basis.thy	Sun Nov 26 13:19:52 2017 +0100
     1.2 +++ b/src/HOL/Groebner_Basis.thy	Sun Nov 26 21:08:32 2017 +0100
     1.3 @@ -19,8 +19,8 @@
     1.4    by blast+
     1.5  
     1.6  lemma dnf:
     1.7 -  "(P & (Q | R)) = ((P&Q) | (P&R))"
     1.8 -  "((Q | R) & P) = ((Q&P) | (R&P))"
     1.9 +  "(P \<and> (Q \<or> R)) = ((P\<and>Q) \<or> (P\<and>R))"
    1.10 +  "((Q \<or> R) \<and> P) = ((Q\<and>P) \<or> (R\<and>P))"
    1.11    "(P \<and> Q) = (Q \<and> P)"
    1.12    "(P \<or> Q) = (Q \<or> P)"
    1.13    by blast+