--- a/src/HOL/GCD.thy Sun Aug 25 21:27:25 2024 +0100 +++ b/src/HOL/GCD.thy Sun Aug 25 23:19:33 2024 +0200 @@ -2933,7 +2933,7 @@ end -lemma (in semiring_char_0) CHAR_eq_0 [simp]: "semiring_char TYPE('a) = 0" +lemma (in semiring_char_0) CHAR_eq_0 [simp]: "CHAR('a) = 0" by (simp add: CHAR_eq0_iff)