summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

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))" 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)