# HG changeset patch
# User wenzelm
# Date 1442497644 -7200
# Node ID b34551d94934adc719c980f57efe8736e0c4df68
# Parent  ff00ad5dc03a1c0bd42ff5f8c44051aca793bd97
isabelle update_cartouches;

diff -r ff00ad5dc03a -r b34551d94934 src/HOL/Library/Extended_Real.thy
--- a/src/HOL/Library/Extended_Real.thy	Wed Sep 16 23:48:35 2015 +0200
+++ b/src/HOL/Library/Extended_Real.thy	Thu Sep 17 15:47:24 2015 +0200
@@ -2195,7 +2195,7 @@
   show "ereal_of_enat (Sup A) \<le> (SUP a : A. ereal_of_enat a)"
   proof cases
     assume "finite A"
-    with `A \<noteq> {}` obtain a where "a \<in> A" "ereal_of_enat (Sup A) = ereal_of_enat a"
+    with \<open>A \<noteq> {}\<close> obtain a where "a \<in> A" "ereal_of_enat (Sup A) = ereal_of_enat a"
       using Max_in[of A] by (auto simp: Sup_enat_def simp del: Max_in)
     then show ?thesis
       by (auto intro: SUP_upper)
@@ -2208,11 +2208,11 @@
       then obtain n :: nat where "x < n"
         using less_PInf_Ex_of_nat top_ereal_def by auto
       obtain a where "a \<in> A - enat ` {.. n}"
-        by (metis `\<not> finite A` all_not_in_conv finite_Diff2 finite_atMost finite_imageI finite.emptyI)
+        by (metis \<open>\<not> finite A\<close> all_not_in_conv finite_Diff2 finite_atMost finite_imageI finite.emptyI)
       then have "a \<in> A" "ereal n \<le> ereal_of_enat a"
         by (auto simp: image_iff Ball_def)
            (metis enat_iless enat_ord_simps(1) ereal_of_enat_less_iff ereal_of_enat_simps(1) less_le not_less)
-      with `x < n` show "\<exists>i\<in>A. x < ereal_of_enat i"
+      with \<open>x < n\<close> show "\<exists>i\<in>A. x < ereal_of_enat i"
         by (auto intro!: bexI[of _ a])
     qed
     show ?thesis
diff -r ff00ad5dc03a -r b34551d94934 src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Wed Sep 16 23:48:35 2015 +0200
+++ b/src/HOL/Library/Multiset.thy	Thu Sep 17 15:47:24 2015 +0200
@@ -1408,14 +1408,14 @@
 proof (rule properties_for_sort_key)
   from mset_equal
   show "mset ys = mset xs" by simp
-  from `sorted (map f ys)`
+  from \<open>sorted (map f ys)\<close>
   show "sorted (map f ys)" .
   show "[x\<leftarrow>ys . f k = f x] = [x\<leftarrow>xs . f k = f x]" if "k \<in> set ys" for k
   proof -
     from mset_equal
     have set_equal: "set xs = set ys" by (rule mset_eq_setD)
     with that have "insert k (set ys) = set ys" by auto
-    with `inj_on f (set xs)` have inj: "inj_on f (insert k (set ys))"
+    with \<open>inj_on f (set xs)\<close> have inj: "inj_on f (insert k (set ys))"
       by (simp add: set_equal)
     from inj have "[x\<leftarrow>ys . f k = f x] = filter (HOL.eq k) ys"
       by (auto intro!: inj_on_filter_key_eq)