removed duplicate lemma
authorkrauss
Sun Sep 05 21:39:24 2010 +0200 (2010-09-05)
changeset 39150c4ff5fd8db99
parent 39149 aabd6d4a5c3a
child 39151 fd179beb8cb3
removed duplicate lemma
NEWS
src/HOL/Option.thy
     1.1 --- a/NEWS	Sun Sep 05 21:39:16 2010 +0200
     1.2 +++ b/NEWS	Sun Sep 05 21:39:24 2010 +0200
     1.3 @@ -166,6 +166,9 @@
     1.4  (class eq) carry proper names and are treated as default code
     1.5  equations.
     1.6  
     1.7 +* Removed lemma Option.is_none_none (Duplicate of is_none_def).
     1.8 +INCOMPATIBILITY.
     1.9 +
    1.10  * List.thy: use various operations from the Haskell prelude when
    1.11  generating Haskell code.
    1.12  
     2.1 --- a/src/HOL/Option.thy	Sun Sep 05 21:39:16 2010 +0200
     2.2 +++ b/src/HOL/Option.thy	Sun Sep 05 21:39:24 2010 +0200
     2.3 @@ -106,13 +106,9 @@
     2.4      and "is_none (Some x) \<longleftrightarrow> False"
     2.5    unfolding is_none_def by simp_all
     2.6  
     2.7 -lemma is_none_none:
     2.8 -  "is_none x \<longleftrightarrow> x = None"
     2.9 -  by (simp add: is_none_def)
    2.10 -
    2.11  lemma [code_unfold]:
    2.12    "HOL.equal x None \<longleftrightarrow> is_none x"
    2.13 -  by (simp add: equal is_none_none)
    2.14 +  by (simp add: equal is_none_def)
    2.15  
    2.16  hide_const (open) is_none
    2.17