NEWS

 been the case with "split".  INCOMPATIBILITY.
 
 * Datatype package: theorems generated for executable equality
 (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.
 
 * code_simp.ML and method code_simp: simplification with rules determined