isabelle update_cartouches -c -t;
authorwenzelm
Tue Aug 01 17:33:04 2017 +0200 (23 months ago)
changeset 66304cde6ceffcbc7
parent 66303 210dae34b8bc
child 66305 7454317f883c
isabelle update_cartouches -c -t;
src/HOL/Analysis/Improper_Integral.thy
src/HOL/Analysis/Topology_Euclidean_Space.thy
src/HOL/Analysis/Winding_Numbers.thy
src/HOL/Number_Theory/Residues.thy
     1.1 --- a/src/HOL/Analysis/Improper_Integral.thy	Tue Aug 01 17:30:02 2017 +0200
     1.2 +++ b/src/HOL/Analysis/Improper_Integral.thy	Tue Aug 01 17:33:04 2017 +0200
     1.3 @@ -1498,7 +1498,7 @@
     1.4        using bounded_integrals_over_subintervals [OF int_gab] unfolding bounded_pos real_norm_def by blast
     1.5      show "(\<lambda>x. f x \<bullet> j) absolutely_integrable_on cbox a b"
     1.6        using g
     1.7 -    proof     --\<open>A lot of duplication in the two proofs\<close>
     1.8 +    proof     \<comment>\<open>A lot of duplication in the two proofs\<close>
     1.9        assume fg [rule_format]: "\<forall>x\<in>cbox a b. f x \<bullet> j \<le> g x"
    1.10        have "(\<lambda>x. (f x \<bullet> j)) = (\<lambda>x. g x - (g x - (f x \<bullet> j)))"
    1.11          by simp
     2.1 --- a/src/HOL/Analysis/Topology_Euclidean_Space.thy	Tue Aug 01 17:30:02 2017 +0200
     2.2 +++ b/src/HOL/Analysis/Topology_Euclidean_Space.thy	Tue Aug 01 17:33:04 2017 +0200
     2.3 @@ -5300,7 +5300,7 @@
     2.4    "compact (s :: 'a::metric_space set) \<longleftrightarrow> seq_compact s"
     2.5    using compact_imp_seq_compact seq_compact_imp_heine_borel by blast
     2.6  
     2.7 -lemma compact_def: --\<open>this is the definition of compactness in HOL Light\<close>
     2.8 +lemma compact_def: \<comment>\<open>this is the definition of compactness in HOL Light\<close>
     2.9    "compact (S :: 'a::metric_space set) \<longleftrightarrow>
    2.10     (\<forall>f. (\<forall>n. f n \<in> S) \<longrightarrow> (\<exists>l\<in>S. \<exists>r. subseq r \<and> (f \<circ> r) \<longlonglongrightarrow> l))"
    2.11    unfolding compact_eq_seq_compact_metric seq_compact_def by auto
     3.1 --- a/src/HOL/Analysis/Winding_Numbers.thy	Tue Aug 01 17:30:02 2017 +0200
     3.2 +++ b/src/HOL/Analysis/Winding_Numbers.thy	Tue Aug 01 17:33:04 2017 +0200
     3.3 @@ -41,7 +41,7 @@
     3.4            by (meson mem_interior)
     3.5          define z where "z \<equiv> - sgn (Im b) * (e/3) + sgn (Re b) * (e/3) * \<i>"
     3.6          have "z \<in> ball 0 e"
     3.7 -          using `e>0`
     3.8 +          using \<open>e>0\<close>
     3.9            apply (simp add: z_def dist_norm)
    3.10            apply (rule le_less_trans [OF norm_triangle_ineq4])
    3.11            apply (simp add: norm_mult abs_sgn_eq)
    3.12 @@ -49,7 +49,7 @@
    3.13          then have "z \<in> {z. Im z * Re b \<le> Im b * Re z}"
    3.14            using e by blast
    3.15          then show False
    3.16 -          using `e>0` `b \<noteq> 0`
    3.17 +          using \<open>e>0\<close> \<open>b \<noteq> 0\<close>
    3.18            apply (simp add: z_def dist_norm sgn_if less_eq_real_def mult_less_0_iff complex.expand split: if_split_asm)
    3.19            apply (auto simp: algebra_simps)
    3.20            apply (meson less_asym less_trans mult_pos_pos neg_less_0_iff_less)
     4.1 --- a/src/HOL/Number_Theory/Residues.thy	Tue Aug 01 17:30:02 2017 +0200
     4.2 +++ b/src/HOL/Number_Theory/Residues.thy	Tue Aug 01 17:33:04 2017 +0200
     4.3 @@ -378,9 +378,9 @@
     4.4      by (metis residues_prime.wilson_theorem1 residues_prime.intro le_eq_less_or_eq)
     4.5  qed
     4.6  
     4.7 -text {*
     4.8 +text \<open>
     4.9    This result can be transferred to the multiplicative group of
    4.10 -  $\mathbb{Z}/p\mathbb{Z}$ for $p$ prime. *}
    4.11 +  $\mathbb{Z}/p\mathbb{Z}$ for $p$ prime.\<close>
    4.12  
    4.13  lemma mod_nat_int_pow_eq:
    4.14    fixes n :: nat and p a :: int
    4.15 @@ -409,22 +409,22 @@
    4.16    have **:"nat ` {1 .. int p - 1} = {1 .. p - 1}" (is "?L = ?R")
    4.17    proof
    4.18      { fix n assume n: "n \<in> ?L"
    4.19 -      then have "n \<in> ?R" using `p\<ge>2` by force
    4.20 +      then have "n \<in> ?R" using \<open>p\<ge>2\<close> by force
    4.21      } thus "?L \<subseteq> ?R" by blast
    4.22      { fix n assume n: "n \<in> ?R"
    4.23 -      then have "n \<in> ?L" using `p\<ge>2` Set_Interval.transfer_nat_int_set_functions(2) by fastforce
    4.24 +      then have "n \<in> ?L" using \<open>p\<ge>2\<close> Set_Interval.transfer_nat_int_set_functions(2) by fastforce
    4.25      } thus "?R \<subseteq> ?L" by blast
    4.26    qed
    4.27    have "nat ` {a^i mod (int p) | i::nat. i \<in> UNIV} = {nat a^i mod p | i . i \<in> UNIV}" (is "?L = ?R")
    4.28    proof
    4.29      { fix x assume x: "x \<in> ?L"
    4.30        then obtain i where i:"x = nat (a^i mod (int p))" by blast
    4.31 -      hence "x = nat a ^ i mod p" using mod_nat_int_pow_eq[of a "int p" i] a `p\<ge>2` by auto
    4.32 +      hence "x = nat a ^ i mod p" using mod_nat_int_pow_eq[of a "int p" i] a \<open>p\<ge>2\<close> by auto
    4.33        hence "x \<in> ?R" using i by blast
    4.34      } thus "?L \<subseteq> ?R" by blast
    4.35      { fix x assume x: "x \<in> ?R"
    4.36        then obtain i where i:"x = nat a^i mod p" by blast
    4.37 -      hence "x \<in> ?L" using mod_nat_int_pow_eq[of a "int p" i] a `p\<ge>2` by auto
    4.38 +      hence "x \<in> ?L" using mod_nat_int_pow_eq[of a "int p" i] a \<open>p\<ge>2\<close> by auto
    4.39      } thus "?R \<subseteq> ?L" by blast
    4.40    qed
    4.41    hence "{1 .. p - 1} = {nat a^i mod p | i. i \<in> UNIV}"