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