diff -r 787a203a20b6 -r c530cb79ccbc src/HOL/Rings.thy --- a/src/HOL/Rings.thy Mon Aug 22 21:37:06 2022 +0200 +++ b/src/HOL/Rings.thy Wed Aug 24 06:21:06 2022 +0000 @@ -382,7 +382,7 @@ subclass semiring_1_cancel .. -lemma of_bool_not_iff [simp]: +lemma of_bool_not_iff: \of_bool (\ P) = 1 - of_bool P\ by simp