changeset 82774 | 2865a6618cba |
parent 81706 | 7beb0cf38292 |
--- 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 \<longleftrightarrow> True" + "is_none (Some x) \<longleftrightarrow> False" by simp_all lemma rel_option_unfold: