--- 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.
--- 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