isabelle update_cartouches -c -t;
authorwenzelm
Wed May 25 11:49:40 2016 +0200 (2016-05-25)
changeset 63145703edebd1d92
parent 63143 ef72b104fa32
child 63146 f1ecba0272f9
isabelle update_cartouches -c -t;
src/HOL/Divides.thy
src/HOL/GCD.thy
src/HOL/Groups.thy
src/HOL/Library/Disjoint_Sets.thy
src/HOL/Library/Extended_Nonnegative_Real.thy
src/HOL/Library/Extended_Real.thy
src/HOL/Library/Polynomial.thy
src/HOL/Library/Stirling.thy
src/HOL/List.thy
src/HOL/Multivariate_Analysis/Polytope.thy
src/HOL/Nat.thy
src/HOL/Series.thy
src/HOL/Transcendental.thy
     1.1 --- a/src/HOL/Divides.thy	Tue May 24 22:46:23 2016 +0200
     1.2 +++ b/src/HOL/Divides.thy	Wed May 25 11:49:40 2016 +0200
     1.3 @@ -1637,7 +1637,7 @@
     1.4    shows "Suc 0 mod numeral k = snd (divmod Num.One k)"
     1.5    by (simp_all add: snd_divmod)
     1.6  
     1.7 -lemma cut_eq_simps: -- \<open>rewriting equivalence on @{text "n mod 2 ^ q"}\<close>
     1.8 +lemma cut_eq_simps: \<comment> \<open>rewriting equivalence on \<open>n mod 2 ^ q\<close>\<close>
     1.9    fixes m n q :: num
    1.10    shows
    1.11      "numeral n mod numeral Num.One = (0::nat)
     2.1 --- a/src/HOL/GCD.thy	Tue May 24 22:46:23 2016 +0200
     2.2 +++ b/src/HOL/GCD.thy	Wed May 25 11:49:40 2016 +0200
     2.3 @@ -1590,7 +1590,7 @@
     2.4  
     2.5  (* to do: add the three variations of these, and for ints? *)
     2.6  
     2.7 -lemma finite_divisors_nat [simp]: -- \<open>FIXME move\<close>
     2.8 +lemma finite_divisors_nat [simp]: \<comment> \<open>FIXME move\<close>
     2.9    fixes m :: nat
    2.10    assumes "m > 0" 
    2.11    shows "finite {d. d dvd m}"
    2.12 @@ -1962,7 +1962,7 @@
    2.13    apply auto
    2.14    done
    2.15  
    2.16 -lemma dvd_pos_nat: -- \<open>FIXME move\<close>
    2.17 +lemma dvd_pos_nat: \<comment> \<open>FIXME move\<close>
    2.18    fixes n m :: nat
    2.19    assumes "n > 0" and "m dvd n"
    2.20    shows "m > 0"
     3.1 --- a/src/HOL/Groups.thy	Tue May 24 22:46:23 2016 +0200
     3.2 +++ b/src/HOL/Groups.thy	Wed May 25 11:49:40 2016 +0200
     3.3 @@ -1378,7 +1378,7 @@
     3.4    using add_eq_0_iff_both_eq_0[of m] by (auto simp: le_iff_add less_le)
     3.5  
     3.6  lemmas zero_order = zero_le le_zero_eq not_less_zero zero_less_iff_neq_zero not_gr_zero
     3.7 -  -- \<open>This should be attributed with \<open>[iff]\<close>, but then \<open>blast\<close> fails in \<open>Set\<close>.\<close>
     3.8 +  \<comment> \<open>This should be attributed with \<open>[iff]\<close>, but then \<open>blast\<close> fails in \<open>Set\<close>.\<close>
     3.9  
    3.10  end
    3.11  
     4.1 --- a/src/HOL/Library/Disjoint_Sets.thy	Tue May 24 22:46:23 2016 +0200
     4.2 +++ b/src/HOL/Library/Disjoint_Sets.thy	Wed May 25 11:49:40 2016 +0200
     4.3 @@ -168,7 +168,7 @@
     4.4    proof (rule inj_onI, rule ccontr)
     4.5      fix x y assume A: "x \<in> A" "y \<in> A" "g x = g y" "x \<noteq> y"
     4.6      with g[of x] g[of y] have "g x \<in> f x" "g x \<in> f y" by auto
     4.7 -    with A `x \<noteq> y` assms show False
     4.8 +    with A \<open>x \<noteq> y\<close> assms show False
     4.9        by (auto simp: disjoint_family_on_def inj_on_def)
    4.10    qed
    4.11    from g have "g ` A \<subseteq> UNION A f" by blast
     5.1 --- a/src/HOL/Library/Extended_Nonnegative_Real.thy	Tue May 24 22:46:23 2016 +0200
     5.2 +++ b/src/HOL/Library/Extended_Nonnegative_Real.thy	Wed May 25 11:49:40 2016 +0200
     5.3 @@ -324,7 +324,7 @@
     5.4  
     5.5  end
     5.6  
     5.7 -lemma ennreal_zero_less_one: "0 < (1::ennreal)" -- \<open>TODO: remove \<close>
     5.8 +lemma ennreal_zero_less_one: "0 < (1::ennreal)" \<comment> \<open>TODO: remove \<close>
     5.9    by transfer auto
    5.10  
    5.11  instance ennreal :: dioid
    5.12 @@ -1748,7 +1748,7 @@
    5.13  proof (rule order_tendstoI)
    5.14    fix e::ennreal assume "e > 0"
    5.15    obtain e'::real where "e' > 0" "ennreal e' < e"
    5.16 -    using `0 < e` dense[of 0 "if e = top then 1 else (enn2real e)"]
    5.17 +    using \<open>0 < e\<close> dense[of 0 "if e = top then 1 else (enn2real e)"]
    5.18      by (cases e) (auto simp: ennreal_less_iff)
    5.19    from ev[OF \<open>e' > 0\<close>] show "\<forall>\<^sub>F x in F. f x < e"
    5.20      by eventually_elim (insert \<open>ennreal e' < e\<close>, auto)
     6.1 --- a/src/HOL/Library/Extended_Real.thy	Tue May 24 22:46:23 2016 +0200
     6.2 +++ b/src/HOL/Library/Extended_Real.thy	Wed May 25 11:49:40 2016 +0200
     6.3 @@ -3552,7 +3552,7 @@
     6.4    using Liminf_le_Limsup[OF assms, of f]
     6.5    by auto
     6.6  
     6.7 -lemma convergent_ereal: -- \<open>RENAME\<close>
     6.8 +lemma convergent_ereal: \<comment> \<open>RENAME\<close>
     6.9    fixes X :: "nat \<Rightarrow> 'a :: {complete_linorder,linorder_topology}"
    6.10    shows "convergent X \<longleftrightarrow> limsup X = liminf X"
    6.11    using tendsto_iff_Liminf_eq_Limsup[of sequentially]
     7.1 --- a/src/HOL/Library/Polynomial.thy	Tue May 24 22:46:23 2016 +0200
     7.2 +++ b/src/HOL/Library/Polynomial.thy	Wed May 25 11:49:40 2016 +0200
     7.3 @@ -443,7 +443,7 @@
     7.4    by (simp add: is_zero_def null_def)
     7.5  
     7.6  subsubsection \<open>Reconstructing the polynomial from the list\<close>
     7.7 -  -- \<open>contributed by Sebastiaan J.C. Joosten and René Thiemann\<close>
     7.8 +  \<comment> \<open>contributed by Sebastiaan J.C. Joosten and René Thiemann\<close>
     7.9  
    7.10  definition poly_of_list :: "'a::comm_monoid_add list \<Rightarrow> 'a poly"
    7.11  where
     8.1 --- a/src/HOL/Library/Stirling.thy	Tue May 24 22:46:23 2016 +0200
     8.2 +++ b/src/HOL/Library/Stirling.thy	Wed May 25 11:49:40 2016 +0200
     8.3 @@ -1,13 +1,13 @@
     8.4  (* Authors: Amine Chaieb & Florian Haftmann, TU Muenchen
     8.5              with contributions by Lukas Bulwahn and Manuel Eberl*)
     8.6  
     8.7 -section {* Stirling numbers of first and second kind *}
     8.8 +section \<open>Stirling numbers of first and second kind\<close>
     8.9  
    8.10  theory Stirling
    8.11  imports Binomial
    8.12  begin
    8.13  
    8.14 -subsection {* Stirling numbers of the second kind *}
    8.15 +subsection \<open>Stirling numbers of the second kind\<close>
    8.16  
    8.17  fun Stirling :: "nat \<Rightarrow> nat \<Rightarrow> nat"
    8.18  where
    8.19 @@ -54,7 +54,7 @@
    8.20    "Stirling (Suc n) (Suc (Suc 0)) = 2 ^ n - 1"
    8.21    using Stirling_2_2 by (cases n) simp_all
    8.22  
    8.23 -subsection {* Stirling numbers of the first kind *}
    8.24 +subsection \<open>Stirling numbers of the first kind\<close>
    8.25  
    8.26  fun stirling :: "nat \<Rightarrow> nat \<Rightarrow> nat"
    8.27  where
     9.1 --- a/src/HOL/List.thy	Tue May 24 22:46:23 2016 +0200
     9.2 +++ b/src/HOL/List.thy	Wed May 25 11:49:40 2016 +0200
     9.3 @@ -3006,7 +3006,7 @@
     9.4  lemma upt_conv_Cons: "i < j ==> [i..<j] = i # [Suc i..<j]"
     9.5  by (simp add: upt_rec)
     9.6  
     9.7 -lemma upt_conv_Cons_Cons: -- \<open>no precondition\<close>
     9.8 +lemma upt_conv_Cons_Cons: \<comment> \<open>no precondition\<close>
     9.9    "m # n # ns = [m..<q] \<longleftrightarrow> n # ns = [Suc m..<q]"
    9.10  proof (cases "m < q")
    9.11    case False then show ?thesis by simp
    10.1 --- a/src/HOL/Multivariate_Analysis/Polytope.thy	Tue May 24 22:46:23 2016 +0200
    10.2 +++ b/src/HOL/Multivariate_Analysis/Polytope.thy	Wed May 25 11:49:40 2016 +0200
    10.3 @@ -99,7 +99,7 @@
    10.4        apply (rule zne [OF in01])
    10.5        apply (rule e [THEN subsetD])
    10.6        apply (rule IntI)
    10.7 -        using `y \<noteq> x` \<open>e > 0\<close>
    10.8 +        using \<open>y \<noteq> x\<close> \<open>e > 0\<close>
    10.9          apply (simp add: cball_def dist_norm algebra_simps)
   10.10          apply (simp add: Real_Vector_Spaces.scaleR_diff_right [symmetric] norm_minus_commute min_mult_distrib_right)
   10.11        apply (rule mem_affine [OF affine_affine_hull _ x])
   10.12 @@ -208,7 +208,7 @@
   10.13        done
   10.14      then have "d \<in> T \<and> c \<in> T"
   10.15        apply (rule face_ofD [OF \<open>T face_of S\<close>])
   10.16 -      using `d \<in> u`  `c \<in> u` \<open>u \<subseteq> S\<close>  \<open>b \<in> T\<close>  apply auto
   10.17 +      using \<open>d \<in> u\<close>  \<open>c \<in> u\<close> \<open>u \<subseteq> S\<close>  \<open>b \<in> T\<close>  apply auto
   10.18        done
   10.19      then show ?thesis ..
   10.20    qed
   10.21 @@ -338,7 +338,7 @@
   10.22          then have [simp]: "setsum c (S - T) = 1"
   10.23            by (simp add: S setsum_diff sumc1)
   10.24          have ci0: "\<And>i. i \<in> T \<Longrightarrow> c i = 0"
   10.25 -          by (meson `finite T` `setsum c T = 0` \<open>T \<subseteq> S\<close> cge0 setsum_nonneg_eq_0_iff subsetCE)
   10.26 +          by (meson \<open>finite T\<close> \<open>setsum c T = 0\<close> \<open>T \<subseteq> S\<close> cge0 setsum_nonneg_eq_0_iff subsetCE)
   10.27          then have [simp]: "(\<Sum>i\<in>S-T. c i *\<^sub>R i) = w"
   10.28            by (simp add: weq_sumsum)
   10.29          have "w \<in> convex hull (S - T)"
   10.30 @@ -359,7 +359,7 @@
   10.31            apply (metis sumcf cge0 inverse_nonnegative_iff_nonnegative mult_nonneg_nonneg S(2) setsum_nonneg subsetCE)
   10.32            apply (metis False mult.commute right_inverse right_minus_eq setsum_right_distrib sumcf)
   10.33            by (metis (mono_tags, lifting) scaleR_right.setsum scaleR_scaleR setsum.cong)
   10.34 -        with `0 < k`  have "inverse(k) *\<^sub>R (w - setsum (\<lambda>i. c i *\<^sub>R i) T) \<in> affine hull T"
   10.35 +        with \<open>0 < k\<close>  have "inverse(k) *\<^sub>R (w - setsum (\<lambda>i. c i *\<^sub>R i) T) \<in> affine hull T"
   10.36            by (simp add: affine_diff_divide [OF affine_affine_hull] False waff convex_hull_subset_affine_hull [THEN subsetD])
   10.37          moreover have "inverse(k) *\<^sub>R (w - setsum (\<lambda>x. c x *\<^sub>R x) T) \<in> convex hull (S - T)"
   10.38            apply (simp add: weq_sumsum convex_hull_finite fin)
   10.39 @@ -413,7 +413,7 @@
   10.40      qed
   10.41    qed
   10.42    then show False
   10.43 -    using `T \<noteq> S` \<open>T face_of S\<close> face_of_imp_subset by blast
   10.44 +    using \<open>T \<noteq> S\<close> \<open>T face_of S\<close> face_of_imp_subset by blast
   10.45  qed
   10.46  
   10.47  
   10.48 @@ -2504,11 +2504,11 @@
   10.49    then consider "card S = 0" | "card S = 1" | "2 \<le> card S" by arith
   10.50    then show ?thesis
   10.51    proof cases
   10.52 -    case 1 then have "S = {}" by (simp add: `finite S`)
   10.53 +    case 1 then have "S = {}" by (simp add: \<open>finite S\<close>)
   10.54      then show ?thesis by simp
   10.55    next
   10.56      case 2 show ?thesis
   10.57 -      by (auto intro: card_1_singletonE [OF `card S = 1`])
   10.58 +      by (auto intro: card_1_singletonE [OF \<open>card S = 1\<close>])
   10.59    next
   10.60      case 3
   10.61      with assms show ?thesis
   10.62 @@ -2535,7 +2535,7 @@
   10.63        then have "x \<in> (\<Union>a\<in>S. convex hull (S - {a}))"
   10.64          using True affine_independent_iff_card [of S]
   10.65          apply simp
   10.66 -        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)
   10.67 +        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)
   10.68          done
   10.69      } note * = this
   10.70      have 1: "convex hull S \<subseteq> (\<Union> a\<in>S. convex hull (S - {a}))"
    11.1 --- a/src/HOL/Nat.thy	Tue May 24 22:46:23 2016 +0200
    11.2 +++ b/src/HOL/Nat.thy	Wed May 25 11:49:40 2016 +0200
    11.3 @@ -757,10 +757,10 @@
    11.4  
    11.5  instance nat :: dioid
    11.6    by standard (rule nat_le_iff_add)
    11.7 -declare le0[simp del] -- \<open>This is now @{thm zero_le}\<close>
    11.8 -declare le_0_eq[simp del] -- \<open>This is now @{thm le_zero_eq}\<close>
    11.9 -declare not_less0[simp del] -- \<open>This is now @{thm not_less_zero}\<close>
   11.10 -declare not_gr0[simp del] -- \<open>This is now @{thm not_gr_zero}\<close>
   11.11 +declare le0[simp del] \<comment> \<open>This is now @{thm zero_le}\<close>
   11.12 +declare le_0_eq[simp del] \<comment> \<open>This is now @{thm le_zero_eq}\<close>
   11.13 +declare not_less0[simp del] \<comment> \<open>This is now @{thm not_less_zero}\<close>
   11.14 +declare not_gr0[simp del] \<comment> \<open>This is now @{thm not_gr_zero}\<close>
   11.15  
   11.16  instance nat :: ordered_cancel_comm_monoid_add ..
   11.17  instance nat :: ordered_cancel_comm_monoid_diff ..
    12.1 --- a/src/HOL/Series.thy	Tue May 24 22:46:23 2016 +0200
    12.2 +++ b/src/HOL/Series.thy	Wed May 25 11:49:40 2016 +0200
    12.3 @@ -362,7 +362,7 @@
    12.4  
    12.5  end
    12.6  
    12.7 -context --\<open>Separate contexts are necessary to allow general use of the results above, here.\<close>
    12.8 +context \<comment>\<open>Separate contexts are necessary to allow general use of the results above, here.\<close>
    12.9    fixes f :: "nat \<Rightarrow> 'a::real_normed_vector"
   12.10  begin
   12.11  
    13.1 --- a/src/HOL/Transcendental.thy	Tue May 24 22:46:23 2016 +0200
    13.2 +++ b/src/HOL/Transcendental.thy	Wed May 25 11:49:40 2016 +0200
    13.3 @@ -2471,7 +2471,7 @@
    13.4     from assms have "0 < m"
    13.5       by (metis less_trans zero_less_power less_le_trans zero_less_one)
    13.6     have "n = log b (b ^ n)" using assms(1) by (simp add: log_nat_power)
    13.7 -   also have "\<dots> \<le> log b m" using assms `0 < m` by simp
    13.8 +   also have "\<dots> \<le> log b m" using assms \<open>0 < m\<close> by simp
    13.9     finally show ?thesis .
   13.10  qed
   13.11