src/HOL/Option.thy
changeset 39150 c4ff5fd8db99
parent 39149 aabd6d4a5c3a
child 39159 0dec18004e75
     1.1 --- a/src/HOL/Option.thy	Sun Sep 05 21:39:16 2010 +0200
     1.2 +++ b/src/HOL/Option.thy	Sun Sep 05 21:39:24 2010 +0200
     1.3 @@ -106,13 +106,9 @@
     1.4      and "is_none (Some x) \<longleftrightarrow> False"
     1.5    unfolding is_none_def by simp_all
     1.6  
     1.7 -lemma is_none_none:
     1.8 -  "is_none x \<longleftrightarrow> x = None"
     1.9 -  by (simp add: is_none_def)
    1.10 -
    1.11  lemma [code_unfold]:
    1.12    "HOL.equal x None \<longleftrightarrow> is_none x"
    1.13 -  by (simp add: equal is_none_none)
    1.14 +  by (simp add: equal is_none_def)
    1.15  
    1.16  hide_const (open) is_none
    1.17