# HG changeset patch
# User lammich <lammich@in.tum.de>
# Date 1380195453 -7200
# Node ID 36cf426cb1c67d04ef8108f1948d35cb91a2aed7
# Parent  a268daff3e0f69083d4a05c61d5c9d95f18f57a2
Added symmetric code_unfold-lemmas for null and is_none

diff -r a268daff3e0f -r 36cf426cb1c6 src/HOL/List.thy
--- a/src/HOL/List.thy	Thu Sep 26 11:41:01 2013 +0200
+++ b/src/HOL/List.thy	Thu Sep 26 13:37:33 2013 +0200
@@ -6002,7 +6002,8 @@
 
 lemma equal_Nil_null [code_unfold]:
   "HOL.equal xs [] \<longleftrightarrow> null xs"
-  by (simp add: equal eq_Nil_null)
+  "HOL.equal [] = null"
+  by (auto simp add: equal null_def)
 
 definition maps :: "('a \<Rightarrow> 'b list) \<Rightarrow> 'a list \<Rightarrow> 'b list" where
   [code_abbrev]: "maps f xs = concat (map f xs)"
diff -r a268daff3e0f -r 36cf426cb1c6 src/HOL/Option.thy
--- a/src/HOL/Option.thy	Thu Sep 26 11:41:01 2013 +0200
+++ b/src/HOL/Option.thy	Thu Sep 26 13:37:33 2013 +0200
@@ -187,7 +187,8 @@
 
 lemma [code_unfold]:
   "HOL.equal x None \<longleftrightarrow> is_none x"
-  by (simp add: equal is_none_def)
+  "HOL.equal None = is_none"
+  by (auto simp add: equal is_none_def)
 
 hide_const (open) is_none