src/HOL/Option.thy
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: