# HG changeset patch
# User wenzelm
# Date 1464169780 -7200
# Node ID 703edebd1d925381219bcf190342ed066c733a24
# Parent  ef72b104fa323eb8980b039e776040c372917885
isabelle update_cartouches -c -t;

diff -r ef72b104fa32 -r 703edebd1d92 src/HOL/Divides.thy
--- a/src/HOL/Divides.thy	Tue May 24 22:46:23 2016 +0200
+++ b/src/HOL/Divides.thy	Wed May 25 11:49:40 2016 +0200
@@ -1637,7 +1637,7 @@
   shows "Suc 0 mod numeral k = snd (divmod Num.One k)"
   by (simp_all add: snd_divmod)
 
-lemma cut_eq_simps: -- \<open>rewriting equivalence on @{text "n mod 2 ^ q"}\<close>
+lemma cut_eq_simps: \<comment> \<open>rewriting equivalence on \<open>n mod 2 ^ q\<close>\<close>
   fixes m n q :: num
   shows
     "numeral n mod numeral Num.One = (0::nat)
diff -r ef72b104fa32 -r 703edebd1d92 src/HOL/GCD.thy
--- a/src/HOL/GCD.thy	Tue May 24 22:46:23 2016 +0200
+++ b/src/HOL/GCD.thy	Wed May 25 11:49:40 2016 +0200
@@ -1590,7 +1590,7 @@
 
 (* to do: add the three variations of these, and for ints? *)
 
-lemma finite_divisors_nat [simp]: -- \<open>FIXME move\<close>
+lemma finite_divisors_nat [simp]: \<comment> \<open>FIXME move\<close>
   fixes m :: nat
   assumes "m > 0" 
   shows "finite {d. d dvd m}"
@@ -1962,7 +1962,7 @@
   apply auto
   done
 
-lemma dvd_pos_nat: -- \<open>FIXME move\<close>
+lemma dvd_pos_nat: \<comment> \<open>FIXME move\<close>
   fixes n m :: nat
   assumes "n > 0" and "m dvd n"
   shows "m > 0"
diff -r ef72b104fa32 -r 703edebd1d92 src/HOL/Groups.thy
--- a/src/HOL/Groups.thy	Tue May 24 22:46:23 2016 +0200
+++ b/src/HOL/Groups.thy	Wed May 25 11:49:40 2016 +0200
@@ -1378,7 +1378,7 @@
   using add_eq_0_iff_both_eq_0[of m] by (auto simp: le_iff_add less_le)
 
 lemmas zero_order = zero_le le_zero_eq not_less_zero zero_less_iff_neq_zero not_gr_zero
-  -- \<open>This should be attributed with \<open>[iff]\<close>, but then \<open>blast\<close> fails in \<open>Set\<close>.\<close>
+  \<comment> \<open>This should be attributed with \<open>[iff]\<close>, but then \<open>blast\<close> fails in \<open>Set\<close>.\<close>
 
 end
 
diff -r ef72b104fa32 -r 703edebd1d92 src/HOL/Library/Disjoint_Sets.thy
--- a/src/HOL/Library/Disjoint_Sets.thy	Tue May 24 22:46:23 2016 +0200
+++ b/src/HOL/Library/Disjoint_Sets.thy	Wed May 25 11:49:40 2016 +0200
@@ -168,7 +168,7 @@
   proof (rule inj_onI, rule ccontr)
     fix x y assume A: "x \<in> A" "y \<in> A" "g x = g y" "x \<noteq> y"
     with g[of x] g[of y] have "g x \<in> f x" "g x \<in> f y" by auto
-    with A `x \<noteq> y` assms show False
+    with A \<open>x \<noteq> y\<close> assms show False
       by (auto simp: disjoint_family_on_def inj_on_def)
   qed
   from g have "g ` A \<subseteq> UNION A f" by blast
diff -r ef72b104fa32 -r 703edebd1d92 src/HOL/Library/Extended_Nonnegative_Real.thy
--- a/src/HOL/Library/Extended_Nonnegative_Real.thy	Tue May 24 22:46:23 2016 +0200
+++ b/src/HOL/Library/Extended_Nonnegative_Real.thy	Wed May 25 11:49:40 2016 +0200
@@ -324,7 +324,7 @@
 
 end
 
-lemma ennreal_zero_less_one: "0 < (1::ennreal)" -- \<open>TODO: remove \<close>
+lemma ennreal_zero_less_one: "0 < (1::ennreal)" \<comment> \<open>TODO: remove \<close>
   by transfer auto
 
 instance ennreal :: dioid
@@ -1748,7 +1748,7 @@
 proof (rule order_tendstoI)
   fix e::ennreal assume "e > 0"
   obtain e'::real where "e' > 0" "ennreal e' < e"
-    using `0 < e` dense[of 0 "if e = top then 1 else (enn2real e)"]
+    using \<open>0 < e\<close> dense[of 0 "if e = top then 1 else (enn2real e)"]
     by (cases e) (auto simp: ennreal_less_iff)
   from ev[OF \<open>e' > 0\<close>] show "\<forall>\<^sub>F x in F. f x < e"
     by eventually_elim (insert \<open>ennreal e' < e\<close>, auto)
diff -r ef72b104fa32 -r 703edebd1d92 src/HOL/Library/Extended_Real.thy
--- a/src/HOL/Library/Extended_Real.thy	Tue May 24 22:46:23 2016 +0200
+++ b/src/HOL/Library/Extended_Real.thy	Wed May 25 11:49:40 2016 +0200
@@ -3552,7 +3552,7 @@
   using Liminf_le_Limsup[OF assms, of f]
   by auto
 
-lemma convergent_ereal: -- \<open>RENAME\<close>
+lemma convergent_ereal: \<comment> \<open>RENAME\<close>
   fixes X :: "nat \<Rightarrow> 'a :: {complete_linorder,linorder_topology}"
   shows "convergent X \<longleftrightarrow> limsup X = liminf X"
   using tendsto_iff_Liminf_eq_Limsup[of sequentially]
diff -r ef72b104fa32 -r 703edebd1d92 src/HOL/Library/Polynomial.thy
--- a/src/HOL/Library/Polynomial.thy	Tue May 24 22:46:23 2016 +0200
+++ b/src/HOL/Library/Polynomial.thy	Wed May 25 11:49:40 2016 +0200
@@ -443,7 +443,7 @@
   by (simp add: is_zero_def null_def)
 
 subsubsection \<open>Reconstructing the polynomial from the list\<close>
-  -- \<open>contributed by Sebastiaan J.C. Joosten and René Thiemann\<close>
+  \<comment> \<open>contributed by Sebastiaan J.C. Joosten and René Thiemann\<close>
 
 definition poly_of_list :: "'a::comm_monoid_add list \<Rightarrow> 'a poly"
 where
diff -r ef72b104fa32 -r 703edebd1d92 src/HOL/Library/Stirling.thy
--- a/src/HOL/Library/Stirling.thy	Tue May 24 22:46:23 2016 +0200
+++ b/src/HOL/Library/Stirling.thy	Wed May 25 11:49:40 2016 +0200
@@ -1,13 +1,13 @@
 (* Authors: Amine Chaieb & Florian Haftmann, TU Muenchen
             with contributions by Lukas Bulwahn and Manuel Eberl*)
 
-section {* Stirling numbers of first and second kind *}
+section \<open>Stirling numbers of first and second kind\<close>
 
 theory Stirling
 imports Binomial
 begin
 
-subsection {* Stirling numbers of the second kind *}
+subsection \<open>Stirling numbers of the second kind\<close>
 
 fun Stirling :: "nat \<Rightarrow> nat \<Rightarrow> nat"
 where
@@ -54,7 +54,7 @@
   "Stirling (Suc n) (Suc (Suc 0)) = 2 ^ n - 1"
   using Stirling_2_2 by (cases n) simp_all
 
-subsection {* Stirling numbers of the first kind *}
+subsection \<open>Stirling numbers of the first kind\<close>
 
 fun stirling :: "nat \<Rightarrow> nat \<Rightarrow> nat"
 where
diff -r ef72b104fa32 -r 703edebd1d92 src/HOL/List.thy
--- a/src/HOL/List.thy	Tue May 24 22:46:23 2016 +0200
+++ b/src/HOL/List.thy	Wed May 25 11:49:40 2016 +0200
@@ -3006,7 +3006,7 @@
 lemma upt_conv_Cons: "i < j ==> [i..<j] = i # [Suc i..<j]"
 by (simp add: upt_rec)
 
-lemma upt_conv_Cons_Cons: -- \<open>no precondition\<close>
+lemma upt_conv_Cons_Cons: \<comment> \<open>no precondition\<close>
   "m # n # ns = [m..<q] \<longleftrightarrow> n # ns = [Suc m..<q]"
 proof (cases "m < q")
   case False then show ?thesis by simp
diff -r ef72b104fa32 -r 703edebd1d92 src/HOL/Multivariate_Analysis/Polytope.thy
--- a/src/HOL/Multivariate_Analysis/Polytope.thy	Tue May 24 22:46:23 2016 +0200
+++ b/src/HOL/Multivariate_Analysis/Polytope.thy	Wed May 25 11:49:40 2016 +0200
@@ -99,7 +99,7 @@
       apply (rule zne [OF in01])
       apply (rule e [THEN subsetD])
       apply (rule IntI)
-        using `y \<noteq> x` \<open>e > 0\<close>
+        using \<open>y \<noteq> x\<close> \<open>e > 0\<close>
         apply (simp add: cball_def dist_norm algebra_simps)
         apply (simp add: Real_Vector_Spaces.scaleR_diff_right [symmetric] norm_minus_commute min_mult_distrib_right)
       apply (rule mem_affine [OF affine_affine_hull _ x])
@@ -208,7 +208,7 @@
       done
     then have "d \<in> T \<and> c \<in> T"
       apply (rule face_ofD [OF \<open>T face_of S\<close>])
-      using `d \<in> u`  `c \<in> u` \<open>u \<subseteq> S\<close>  \<open>b \<in> T\<close>  apply auto
+      using \<open>d \<in> u\<close>  \<open>c \<in> u\<close> \<open>u \<subseteq> S\<close>  \<open>b \<in> T\<close>  apply auto
       done
     then show ?thesis ..
   qed
@@ -338,7 +338,7 @@
         then have [simp]: "setsum c (S - T) = 1"
           by (simp add: S setsum_diff sumc1)
         have ci0: "\<And>i. i \<in> T \<Longrightarrow> c i = 0"
-          by (meson `finite T` `setsum c T = 0` \<open>T \<subseteq> S\<close> cge0 setsum_nonneg_eq_0_iff subsetCE)
+          by (meson \<open>finite T\<close> \<open>setsum c T = 0\<close> \<open>T \<subseteq> S\<close> cge0 setsum_nonneg_eq_0_iff subsetCE)
         then have [simp]: "(\<Sum>i\<in>S-T. c i *\<^sub>R i) = w"
           by (simp add: weq_sumsum)
         have "w \<in> convex hull (S - T)"
@@ -359,7 +359,7 @@
           apply (metis sumcf cge0 inverse_nonnegative_iff_nonnegative mult_nonneg_nonneg S(2) setsum_nonneg subsetCE)
           apply (metis False mult.commute right_inverse right_minus_eq setsum_right_distrib sumcf)
           by (metis (mono_tags, lifting) scaleR_right.setsum scaleR_scaleR setsum.cong)
-        with `0 < k`  have "inverse(k) *\<^sub>R (w - setsum (\<lambda>i. c i *\<^sub>R i) T) \<in> affine hull T"
+        with \<open>0 < k\<close>  have "inverse(k) *\<^sub>R (w - setsum (\<lambda>i. c i *\<^sub>R i) T) \<in> affine hull T"
           by (simp add: affine_diff_divide [OF affine_affine_hull] False waff convex_hull_subset_affine_hull [THEN subsetD])
         moreover have "inverse(k) *\<^sub>R (w - setsum (\<lambda>x. c x *\<^sub>R x) T) \<in> convex hull (S - T)"
           apply (simp add: weq_sumsum convex_hull_finite fin)
@@ -413,7 +413,7 @@
     qed
   qed
   then show False
-    using `T \<noteq> S` \<open>T face_of S\<close> face_of_imp_subset by blast
+    using \<open>T \<noteq> S\<close> \<open>T face_of S\<close> face_of_imp_subset by blast
 qed
 
 
@@ -2504,11 +2504,11 @@
   then consider "card S = 0" | "card S = 1" | "2 \<le> card S" by arith
   then show ?thesis
   proof cases
-    case 1 then have "S = {}" by (simp add: `finite S`)
+    case 1 then have "S = {}" by (simp add: \<open>finite S\<close>)
     then show ?thesis by simp
   next
     case 2 show ?thesis
-      by (auto intro: card_1_singletonE [OF `card S = 1`])
+      by (auto intro: card_1_singletonE [OF \<open>card S = 1\<close>])
   next
     case 3
     with assms show ?thesis
@@ -2535,7 +2535,7 @@
       then have "x \<in> (\<Union>a\<in>S. convex hull (S - {a}))"
         using True affine_independent_iff_card [of S]
         apply simp
-        apply (metis (no_types, hide_lams) Diff_eq_empty_iff Diff_insert0 `a \<notin> T` `T \<subseteq> S` `x \<in> convex hull T`  hull_mono insert_Diff_single   subsetCE)
+        apply (metis (no_types, hide_lams) Diff_eq_empty_iff Diff_insert0 \<open>a \<notin> T\<close> \<open>T \<subseteq> S\<close> \<open>x \<in> convex hull T\<close>  hull_mono insert_Diff_single   subsetCE)
         done
     } note * = this
     have 1: "convex hull S \<subseteq> (\<Union> a\<in>S. convex hull (S - {a}))"
diff -r ef72b104fa32 -r 703edebd1d92 src/HOL/Nat.thy
--- a/src/HOL/Nat.thy	Tue May 24 22:46:23 2016 +0200
+++ b/src/HOL/Nat.thy	Wed May 25 11:49:40 2016 +0200
@@ -757,10 +757,10 @@
 
 instance nat :: dioid
   by standard (rule nat_le_iff_add)
-declare le0[simp del] -- \<open>This is now @{thm zero_le}\<close>
-declare le_0_eq[simp del] -- \<open>This is now @{thm le_zero_eq}\<close>
-declare not_less0[simp del] -- \<open>This is now @{thm not_less_zero}\<close>
-declare not_gr0[simp del] -- \<open>This is now @{thm not_gr_zero}\<close>
+declare le0[simp del] \<comment> \<open>This is now @{thm zero_le}\<close>
+declare le_0_eq[simp del] \<comment> \<open>This is now @{thm le_zero_eq}\<close>
+declare not_less0[simp del] \<comment> \<open>This is now @{thm not_less_zero}\<close>
+declare not_gr0[simp del] \<comment> \<open>This is now @{thm not_gr_zero}\<close>
 
 instance nat :: ordered_cancel_comm_monoid_add ..
 instance nat :: ordered_cancel_comm_monoid_diff ..
diff -r ef72b104fa32 -r 703edebd1d92 src/HOL/Series.thy
--- a/src/HOL/Series.thy	Tue May 24 22:46:23 2016 +0200
+++ b/src/HOL/Series.thy	Wed May 25 11:49:40 2016 +0200
@@ -362,7 +362,7 @@
 
 end
 
-context --\<open>Separate contexts are necessary to allow general use of the results above, here.\<close>
+context \<comment>\<open>Separate contexts are necessary to allow general use of the results above, here.\<close>
   fixes f :: "nat \<Rightarrow> 'a::real_normed_vector"
 begin
 
diff -r ef72b104fa32 -r 703edebd1d92 src/HOL/Transcendental.thy
--- a/src/HOL/Transcendental.thy	Tue May 24 22:46:23 2016 +0200
+++ b/src/HOL/Transcendental.thy	Wed May 25 11:49:40 2016 +0200
@@ -2471,7 +2471,7 @@
    from assms have "0 < m"
      by (metis less_trans zero_less_power less_le_trans zero_less_one)
    have "n = log b (b ^ n)" using assms(1) by (simp add: log_nat_power)
-   also have "\<dots> \<le> log b m" using assms `0 < m` by simp
+   also have "\<dots> \<le> log b m" using assms \<open>0 < m\<close> by simp
    finally show ?thesis .
 qed