# HG changeset patch
# User krauss
# Date 1283715564 -7200
# Node ID c4ff5fd8db9962ca92c53851bf1970269285af07
# Parent  aabd6d4a5c3abcfcbb6cc969281bf8c2b4959d34
removed duplicate lemma

diff -r aabd6d4a5c3a -r c4ff5fd8db99 NEWS
--- a/NEWS	Sun Sep 05 21:39:16 2010 +0200
+++ b/NEWS	Sun Sep 05 21:39:24 2010 +0200
@@ -166,6 +166,9 @@
 (class eq) carry proper names and are treated as default code
 equations.
 
+* Removed lemma Option.is_none_none (Duplicate of is_none_def).
+INCOMPATIBILITY.
+
 * List.thy: use various operations from the Haskell prelude when
 generating Haskell code.
 
diff -r aabd6d4a5c3a -r c4ff5fd8db99 src/HOL/Option.thy
--- a/src/HOL/Option.thy	Sun Sep 05 21:39:16 2010 +0200
+++ b/src/HOL/Option.thy	Sun Sep 05 21:39:24 2010 +0200
@@ -106,13 +106,9 @@
     and "is_none (Some x) \<longleftrightarrow> False"
   unfolding is_none_def by simp_all
 
-lemma is_none_none:
-  "is_none x \<longleftrightarrow> x = None"
-  by (simp add: is_none_def)
-
 lemma [code_unfold]:
   "HOL.equal x None \<longleftrightarrow> is_none x"
-  by (simp add: equal is_none_none)
+  by (simp add: equal is_none_def)
 
 hide_const (open) is_none