# HG changeset patch
# User wenzelm
# Date 1394009988 -3600
# Node ID c1409c103b77d2d676fb0a522c8df42d0f98a1df
# Parent  e12a0ab9917cfd901ab720b1f593f630f729db66
proper UTF-8;

diff -r e12a0ab9917c -r c1409c103b77 CONTRIBUTORS
--- a/CONTRIBUTORS	Tue Mar 04 16:16:05 2014 -0800
+++ b/CONTRIBUTORS	Wed Mar 05 09:59:48 2014 +0100
@@ -6,13 +6,14 @@
 Contributions to this Isabelle version
 --------------------------------------
 
-* March 2014: René Thiemann
+* March 2014: René Thiemann
   Improved code generation for multisets.
 
 * January 2014: Lars Hupel, TUM
   An improved, interactive simplifier trace with integration into the
   Isabelle/jEdit Prover IDE.
 
+
 Contributions to Isabelle2013-1
 -------------------------------
 
diff -r e12a0ab9917c -r c1409c103b77 src/HOL/Library/Dlist.thy
--- a/src/HOL/Library/Dlist.thy	Tue Mar 04 16:16:05 2014 -0800
+++ b/src/HOL/Library/Dlist.thy	Wed Mar 05 09:59:48 2014 +0100
@@ -154,23 +154,24 @@
   with dxs show "P dxs" by simp
 qed
 
-lemma dlist_case [case_names empty insert, cases type: dlist]:
-  assumes empty: "dxs = empty \<Longrightarrow> P"
-  assumes insert: "\<And>x dys. \<not> member dys x \<Longrightarrow> dxs = insert x dys \<Longrightarrow> P"
-  shows P
+lemma dlist_case [cases type: dlist]:
+  obtains (empty) "dxs = empty"
+    | (insert) x dys where "\<not> member dys x" and "dxs = insert x dys"
 proof (cases dxs)
   case (Abs_dlist xs)
   then have dxs: "dxs = Dlist xs" and distinct: "distinct xs"
     by (simp_all add: Dlist_def distinct_remdups_id)
-  show P proof (cases xs)
-    case Nil with dxs have "dxs = empty" by (simp add: empty_def) 
-    with empty show P .
+  show thesis
+  proof (cases xs)
+    case Nil with dxs
+    have "dxs = empty" by (simp add: empty_def) 
+    with empty show ?thesis .
   next
     case (Cons x xs)
     with dxs distinct have "\<not> member (Dlist xs) x"
       and "dxs = insert x (Dlist xs)"
       by (simp_all add: member_def List.member_def insert_def distinct_remdups_id)
-    with insert show P .
+    with insert show ?thesis .
   qed
 qed
 
diff -r e12a0ab9917c -r c1409c103b77 src/HOL/Library/Extended_Real.thy
--- a/src/HOL/Library/Extended_Real.thy	Tue Mar 04 16:16:05 2014 -0800
+++ b/src/HOL/Library/Extended_Real.thy	Wed Mar 05 09:59:48 2014 +0100
@@ -71,11 +71,10 @@
 lemma inj_ereal[simp]: "inj_on ereal A"
   unfolding inj_on_def by auto
 
-lemma ereal_cases[case_names real PInf MInf, cases type: ereal]:
-  assumes "\<And>r. x = ereal r \<Longrightarrow> P"
-  assumes "x = \<infinity> \<Longrightarrow> P"
-  assumes "x = -\<infinity> \<Longrightarrow> P"
-  shows P
+lemma ereal_cases[cases type: ereal]:
+  obtains (real) r where "x = ereal r"
+    | (PInf) "x = \<infinity>"
+    | (MInf) "x = -\<infinity>"
   using assms by (cases x) auto
 
 lemmas ereal2_cases = ereal_cases[case_product ereal_cases]
diff -r e12a0ab9917c -r c1409c103b77 src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Tue Mar 04 16:16:05 2014 -0800
+++ b/src/HOL/Library/Multiset.thy	Wed Mar 05 09:59:48 2014 +0100
@@ -647,11 +647,10 @@
 lemma multi_nonempty_split: "M \<noteq> {#} \<Longrightarrow> \<exists>A a. M = A + {#a#}"
 by (induct M) auto
 
-lemma multiset_cases [cases type, case_names empty add]:
-assumes em:  "M = {#} \<Longrightarrow> P"
-assumes add: "\<And>N x. M = N + {#x#} \<Longrightarrow> P"
-shows "P"
-using assms by (induct M) simp_all
+lemma multiset_cases [cases type]:
+  obtains (empty) "M = {#}"
+    | (add) N x where "M = N + {#x#}"
+  using assms by (induct M) simp_all
 
 lemma multi_drop_mem_not_eq: "c \<in># B \<Longrightarrow> B - {#c#} \<noteq> B"
 by (cases "B = {#}") (auto dest: multi_member_split)