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 \<and> Q) = of_bool P * of_bool Q"
   by auto