# HG changeset patch # User haftmann # Date 1555143106 0 # Node ID c925bc0df8270dd03eae56b07c6fbb2837c7e6a5 # Parent 0cc7fe6169245fdc897c2e7c1b44c78882403023 tuned diff -r 0cc7fe616924 -r c925bc0df827 src/HOL/Rings.thy --- a/src/HOL/Rings.thy Sat Apr 13 13:30:02 2019 +0200 +++ b/src/HOL/Rings.thy Sat Apr 13 08:11:46 2019 +0000 @@ -120,7 +120,7 @@ class semiring_1 = zero_neq_one + semiring_0 + monoid_mult begin -lemma (in semiring_1) of_bool_conj: +lemma of_bool_conj: "of_bool (P \ Q) = of_bool P * of_bool Q" by auto