changeset 32069 | 6d28bbd33e2c |
parent 31998 | 2c7a24f74db9 |
child 34886 | 873c31d9f10d |
--- a/src/HOL/Option.thy Tue Jul 14 16:27:31 2009 +0200 +++ b/src/HOL/Option.thy Tue Jul 14 16:27:32 2009 +0200 @@ -105,7 +105,7 @@ "is_none x \<longleftrightarrow> x = None" by (simp add: is_none_def) -lemma [code_inline]: +lemma [code_unfold]: "eq_class.eq x None \<longleftrightarrow> is_none x" by (simp add: eq is_none_none)