diff -r 4ec8e654112f -r 2865a6618cba src/HOL/Option.thy --- a/src/HOL/Option.thy Thu Jun 26 17:25:29 2025 +0200 +++ b/src/HOL/Option.thy Thu Jun 26 17:25:29 2025 +0200 @@ -188,8 +188,8 @@ by (simp_all add: is_none_def) lemma is_none_code [code]: - "is_none None = True" - "is_none (Some x) = False" + "is_none None \ True" + "is_none (Some x) \ False" by simp_all lemma rel_option_unfold: