--- 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)
--- 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"
--- 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
--- 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
--- 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)
--- 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]
--- 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
--- 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
--- 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
--- 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}))"
--- 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 ..
--- 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
--- 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