author wenzelm Thu, 17 Sep 2015 15:47:24 +0200 changeset 61188 b34551d94934 parent 61187 ff00ad5dc03a child 61189 9583ddfc07b3
isabelle update_cartouches;
 src/HOL/Library/Extended_Real.thy file | annotate | diff | comparison | revisions src/HOL/Library/Multiset.thy file | annotate | diff | comparison | revisions
--- 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
--- 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))"