src/HOL/Option.thy
changeset 32069 6d28bbd33e2c
parent 31998 2c7a24f74db9
child 34886 873c31d9f10d
equal deleted inserted replaced
32068:98acc234d683 32069:6d28bbd33e2c
   103 
   103 
   104 lemma is_none_none:
   104 lemma is_none_none:
   105   "is_none x \<longleftrightarrow> x = None"
   105   "is_none x \<longleftrightarrow> x = None"
   106   by (simp add: is_none_def)
   106   by (simp add: is_none_def)
   107 
   107 
   108 lemma [code_inline]:
   108 lemma [code_unfold]:
   109   "eq_class.eq x None \<longleftrightarrow> is_none x"
   109   "eq_class.eq x None \<longleftrightarrow> is_none x"
   110   by (simp add: eq is_none_none)
   110   by (simp add: eq is_none_none)
   111 
   111 
   112 hide (open) const is_none
   112 hide (open) const is_none
   113 
   113