# HG changeset patch
# User nipkow
# Date 1284360228 -7200
# Node ID e1bd8a54c40fd07cdade100f6fca1020be052dfc
# Parent  5aefb5bc8a938030c4d7463522846fcb960c4b7c
added and renamed lemmas

diff -r 5aefb5bc8a93 -r e1bd8a54c40f NEWS
--- a/NEWS	Mon Sep 13 06:02:47 2010 +0200
+++ b/NEWS	Mon Sep 13 08:43:48 2010 +0200
@@ -182,6 +182,8 @@
 * List.thy: use various operations from the Haskell prelude when
 generating Haskell code.
 
+* Multiset.thy: renamed empty_idemp -> empty_neutral
+
 * code_simp.ML and method code_simp: simplification with rules determined
 by code generator.
 
diff -r 5aefb5bc8a93 -r e1bd8a54c40f src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Mon Sep 13 06:02:47 2010 +0200
+++ b/src/HOL/Library/Multiset.thy	Mon Sep 13 08:43:48 2010 +0200
@@ -324,6 +324,9 @@
   "B \<le> A \<Longrightarrow> (A::'a multiset) - B + C = A + C - B"
 by (simp add: multiset_ext_iff mset_le_def)
 
+lemma diff_le_self[simp]: "(M::'a multiset) - N \<le> M"
+by(simp add: mset_le_def)
+
 lemma mset_lessD: "A < B \<Longrightarrow> x \<in># A \<Longrightarrow> x \<in># B"
 apply (clarsimp simp: mset_le_def mset_less_def)
 apply (erule_tac x=x in allE)
@@ -1597,7 +1600,7 @@
   thus "(Z + {#}, Z' + {#}) \<in> ms_weak" by (simp add:add_ac)
 qed
 
-lemma empty_idemp: "{#} + x = x" "x + {#} = x"
+lemma empty_neutral: "{#} + x = x" "x + {#} = x"
 and nonempty_plus: "{# x #} + rs \<noteq> {#}"
 and nonempty_single: "{# x #} \<noteq> {#}"
 by auto
@@ -1623,7 +1626,7 @@
 
   val regroup_munion_conv =
       Function_Lib.regroup_conv @{const_abbrev Mempty} @{const_name plus}
-        (map (fn t => t RS eq_reflection) (@{thms add_ac} @ @{thms empty_idemp}))
+        (map (fn t => t RS eq_reflection) (@{thms add_ac} @ @{thms empty_neutral}))
 
   fun unfold_pwleq_tac i =
     (rtac @{thm pw_leq_step} i THEN (fn st => unfold_pwleq_tac (i + 1) st))