# HG changeset patch
# User wenzelm
# Date 1434742893 -7200
# Node ID fad653acf58f8ca3e037317ee49ee6d07e8f5613
# Parent  278b65d9339ce2b8ddf49218e47b32e50480dc1f
isabelle update_cartouches;

diff -r 278b65d9339c -r fad653acf58f src/HOL/Number_Theory/Cong.thy
--- a/src/HOL/Number_Theory/Cong.thy	Fri Jun 19 21:33:03 2015 +0200
+++ b/src/HOL/Number_Theory/Cong.thy	Fri Jun 19 21:41:33 2015 +0200
@@ -23,13 +23,13 @@
 natural numbers and the integers, and added a number of new theorems.
 *)
 
-section {* Congruence *}
+section \<open>Congruence\<close>
 
 theory Cong
 imports Primes
 begin
 
-subsection {* Turn off @{text One_nat_def} *}
+subsection \<open>Turn off @{text One_nat_def}\<close>
 
 lemma power_eq_one_eq_nat [simp]: "((x::nat)^m = 1) = (m = 0 | x = 1)"
   by (induct m) auto
@@ -37,7 +37,7 @@
 declare mod_pos_pos_trivial [simp]
 
 
-subsection {* Main definitions *}
+subsection \<open>Main definitions\<close>
 
 class cong =
   fixes cong :: "'a \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool" ("(1[_ = _] '(()mod _'))")
@@ -74,7 +74,7 @@
 end
 
 
-subsection {* Set up Transfer *}
+subsection \<open>Set up Transfer\<close>
 
 
 lemma transfer_nat_int_cong:
@@ -97,7 +97,7 @@
     transfer_int_nat_cong]
 
 
-subsection {* Congruence *}
+subsection \<open>Congruence\<close>
 
 (* was zcong_0, etc. *)
 lemma cong_0_nat [simp, presburger]: "([(a::nat) = b] (mod 0)) = (a = b)"
@@ -633,20 +633,20 @@
   have "[?x = u1 * 1 + u2 * 0] (mod m1)"
     apply (rule cong_add_nat)
     apply (rule cong_scalar2_nat)
-    apply (rule `[b1 = 1] (mod m1)`)
+    apply (rule \<open>[b1 = 1] (mod m1)\<close>)
     apply (rule cong_scalar2_nat)
-    apply (rule `[b2 = 0] (mod m1)`)
+    apply (rule \<open>[b2 = 0] (mod m1)\<close>)
     done
   then have "[?x = u1] (mod m1)" by simp
   have "[?x = u1 * 0 + u2 * 1] (mod m2)"
     apply (rule cong_add_nat)
     apply (rule cong_scalar2_nat)
-    apply (rule `[b1 = 0] (mod m2)`)
+    apply (rule \<open>[b1 = 0] (mod m2)\<close>)
     apply (rule cong_scalar2_nat)
-    apply (rule `[b2 = 1] (mod m2)`)
+    apply (rule \<open>[b2 = 1] (mod m2)\<close>)
     done
   then have "[?x = u2] (mod m2)" by simp
-  with `[?x = u1] (mod m1)` show ?thesis by blast
+  with \<open>[?x = u1] (mod m1)\<close> show ?thesis by blast
 qed
 
 lemma binary_chinese_remainder_int:
@@ -661,20 +661,20 @@
   have "[?x = u1 * 1 + u2 * 0] (mod m1)"
     apply (rule cong_add_int)
     apply (rule cong_scalar2_int)
-    apply (rule `[b1 = 1] (mod m1)`)
+    apply (rule \<open>[b1 = 1] (mod m1)\<close>)
     apply (rule cong_scalar2_int)
-    apply (rule `[b2 = 0] (mod m1)`)
+    apply (rule \<open>[b2 = 0] (mod m1)\<close>)
     done
   then have "[?x = u1] (mod m1)" by simp
   have "[?x = u1 * 0 + u2 * 1] (mod m2)"
     apply (rule cong_add_int)
     apply (rule cong_scalar2_int)
-    apply (rule `[b1 = 0] (mod m2)`)
+    apply (rule \<open>[b1 = 0] (mod m2)\<close>)
     apply (rule cong_scalar2_int)
-    apply (rule `[b2 = 1] (mod m2)`)
+    apply (rule \<open>[b2 = 1] (mod m2)\<close>)
     done
   then have "[?x = u2] (mod m2)" by simp
-  with `[?x = u1] (mod m1)` show ?thesis by blast
+  with \<open>[?x = u1] (mod m1)\<close> show ?thesis by blast
 qed
 
 lemma cong_modulus_mult_nat: "[(x::nat) = y] (mod m * n) \<Longrightarrow>
@@ -712,7 +712,7 @@
   have one: "[?x = u1] (mod m1)"
     apply (rule cong_trans_nat)
     prefer 2
-    apply (rule `[y = u1] (mod m1)`)
+    apply (rule \<open>[y = u1] (mod m1)\<close>)
     apply (rule cong_modulus_mult_nat)
     apply (rule cong_mod_nat)
     using nz apply auto
@@ -720,7 +720,7 @@
   have two: "[?x = u2] (mod m2)"
     apply (rule cong_trans_nat)
     prefer 2
-    apply (rule `[y = u2] (mod m2)`)
+    apply (rule \<open>[y = u2] (mod m2)\<close>)
     apply (subst mult.commute)
     apply (rule cong_modulus_mult_nat)
     apply (rule cong_mod_nat)
@@ -733,19 +733,19 @@
     assume "[z = u1] (mod m1)" and  "[z = u2] (mod m2)"
     have "[?x = z] (mod m1)"
       apply (rule cong_trans_nat)
-      apply (rule `[?x = u1] (mod m1)`)
+      apply (rule \<open>[?x = u1] (mod m1)\<close>)
       apply (rule cong_sym_nat)
-      apply (rule `[z = u1] (mod m1)`)
+      apply (rule \<open>[z = u1] (mod m1)\<close>)
       done
     moreover have "[?x = z] (mod m2)"
       apply (rule cong_trans_nat)
-      apply (rule `[?x = u2] (mod m2)`)
+      apply (rule \<open>[?x = u2] (mod m2)\<close>)
       apply (rule cong_sym_nat)
-      apply (rule `[z = u2] (mod m2)`)
+      apply (rule \<open>[z = u2] (mod m2)\<close>)
       done
     ultimately have "[?x = z] (mod m1 * m2)"
       by (auto intro: coprime_cong_mult_nat a)
-    with `z < m1 * m2` `?x < m1 * m2` show "z = ?x"
+    with \<open>z < m1 * m2\<close> \<open>?x < m1 * m2\<close> show "z = ?x"
       apply (intro cong_less_modulus_unique_nat)
       apply (auto, erule cong_sym_nat)
       done
diff -r 278b65d9339c -r fad653acf58f src/HOL/Number_Theory/Eratosthenes.thy
--- a/src/HOL/Number_Theory/Eratosthenes.thy	Fri Jun 19 21:33:03 2015 +0200
+++ b/src/HOL/Number_Theory/Eratosthenes.thy	Fri Jun 19 21:41:33 2015 +0200
@@ -2,14 +2,14 @@
     Author:     Florian Haftmann, TU Muenchen
 *)
 
-section {* The sieve of Eratosthenes *}
+section \<open>The sieve of Eratosthenes\<close>
 
 theory Eratosthenes
 imports Main Primes
 begin
 
 
-subsection {* Preliminary: strict divisibility *}
+subsection \<open>Preliminary: strict divisibility\<close>
 
 context dvd
 begin
@@ -20,9 +20,9 @@
 
 end
 
-subsection {* Main corpus *}
+subsection \<open>Main corpus\<close>
 
-text {* The sieve is modelled as a list of booleans, where @{const False} means \emph{marked out}. *}
+text \<open>The sieve is modelled as a list of booleans, where @{const False} means \emph{marked out}.\<close>
 
 type_synonym marks = "bool list"
 
@@ -58,7 +58,7 @@
     intro!: sorted_filter distinct_filter inj_onI sorted_distinct_set_unique)
 
 
-text {* Marking out multiples in a sieve  *}
+text \<open>Marking out multiples in a sieve\<close>
  
 definition mark_out :: "nat \<Rightarrow> marks \<Rightarrow> marks"
 where
@@ -78,7 +78,7 @@
     nth_enumerate_eq less_eq_dvd_minus)
 
 
-text {* Auxiliary operation for efficient implementation  *}
+text \<open>Auxiliary operation for efficient implementation\<close>
 
 definition mark_out_aux :: "nat \<Rightarrow> nat \<Rightarrow> marks \<Rightarrow> marks"
 where
@@ -104,15 +104,15 @@
         assume "\<not> q > 0"
         with q show False by simp
       qed
-      with `n > 0` have "Suc n * q \<ge> 2" by (auto simp add: gr0_conv_Suc)
+      with \<open>n > 0\<close> have "Suc n * q \<ge> 2" by (auto simp add: gr0_conv_Suc)
       with q have a: "a = Suc n * q - 2" by simp
       with B have "q + n * q < n + n + 2"
         by auto
       then have "m * q < m * 2" by (simp add: m_def)
-      with `m > 0` have "q < 2" by simp
-      with `q > 0` have "q = 1" by simp
+      with \<open>m > 0\<close> have "q < 2" by simp
+      with \<open>q > 0\<close> have "q = 1" by simp
       with a have "a = n - 1" by simp
-      with `n > 0` C show False by simp
+      with \<open>n > 0\<close> C show False by simp
     qed
   } note aux = this 
   show ?thesis
@@ -157,7 +157,7 @@
 qed
 
 
-text {* Main entry point to sieve *}
+text \<open>Main entry point to sieve\<close>
 
 fun sieve :: "nat \<Rightarrow> marks \<Rightarrow> marks"
 where
@@ -165,7 +165,7 @@
 | "sieve n (False # bs) = False # sieve (Suc n) bs"
 | "sieve n (True # bs) = True # sieve (Suc n) (mark_out n bs)"
 
-text {*
+text \<open>
   There are the following possible optimisations here:
 
   \begin{itemize}
@@ -179,7 +179,7 @@
   \end{itemize}
 
   This is left as an constructive exercise to the reader.
-*}
+\<close>
 
 lemma numbers_of_marks_sieve:
   "numbers_of_marks (Suc n) (sieve n bs) =
@@ -199,15 +199,15 @@
     assume "n > 0 \<and> n - 1 \<in> M"
     then have "n > 0" and "n - 1 \<in> M" by auto
     then have "Suc (n - 1) \<in> Suc ` M" by blast
-    with `n > 0` show "n \<in> Suc ` M" by simp
+    with \<open>n > 0\<close> show "n \<in> Suc ` M" by simp
   qed
   { fix m :: nat
     assume "Suc (Suc n) \<le> m" and "m dvd Suc n"
-    from `m dvd Suc n` obtain q where "Suc n = m * q" ..
-    with `Suc (Suc n) \<le> m` have "Suc (m * q) \<le> m" by simp
+    from \<open>m dvd Suc n\<close> obtain q where "Suc n = m * q" ..
+    with \<open>Suc (Suc n) \<le> m\<close> have "Suc (m * q) \<le> m" by simp
     then have "m * q < m" by arith
     then have "q = 0" by simp
-    with `Suc n = m * q` have False by simp
+    with \<open>Suc n = m * q\<close> have False by simp
   } note aux1 = this
   { fix m q :: nat
     assume "\<forall>q>0. 1 < q \<longrightarrow> Suc n < q \<longrightarrow> q \<le> Suc (n + length bs)
@@ -219,7 +219,7 @@
     then have "\<not> Suc n dvd q" by (auto elim: dvdE)
     moreover assume "Suc n < q" and "q \<le> Suc (n + length bs)"
       and "bs ! (q - Suc (Suc n))"
-    moreover note `q dvd m`
+    moreover note \<open>q dvd m\<close>
     ultimately have "m dvd q" by (auto intro: *)
   } note aux2 = this
   from 3 show ?case
@@ -234,7 +234,7 @@
 qed
 
 
-text {* Relation of the sieve algorithm to actual primes *}
+text \<open>Relation of the sieve algorithm to actual primes\<close>
 
 definition primes_upto :: "nat \<Rightarrow> nat list"
 where
@@ -267,11 +267,11 @@
     assume *: "\<forall>m\<in>{Suc (Suc 0)..<Suc n}. m dvd q \<longrightarrow> q dvd m"
       and "m dvd q" and "m \<noteq> 1"
     have "m = q" proof (cases "m = 0")
-      case True with `m dvd q` show ?thesis by simp
+      case True with \<open>m dvd q\<close> show ?thesis by simp
     next
-      case False with `m \<noteq> 1` have "Suc (Suc 0) \<le> m" by arith
-      with `m < Suc n` * `m dvd q` have "q dvd m" by simp
-      with `m dvd q` show ?thesis by (simp add: dvd.eq_iff)
+      case False with \<open>m \<noteq> 1\<close> have "Suc (Suc 0) \<le> m" by arith
+      with \<open>m < Suc n\<close> * \<open>m dvd q\<close> have "q dvd m" by simp
+      with \<open>m dvd q\<close> show ?thesis by (simp add: dvd.eq_iff)
     qed
   }
   then have aux: "\<And>m q. Suc (Suc 0) \<le> q \<Longrightarrow>
@@ -303,7 +303,7 @@
   by (simp add: set_primes_upto)
 
 
-subsection {* Application: smallest prime beyond a certain number *}
+subsection \<open>Application: smallest prime beyond a certain number\<close>
 
 definition smallest_prime_beyond :: "nat \<Rightarrow> nat"
 where
@@ -348,7 +348,7 @@
     def A \<equiv> "{p. p \<le> n \<and> prime p \<and> m \<le> p}"
     assume assms: "m \<le> p" "prime p" "p \<le> n"
     then have "smallest_prime_beyond m \<le> p" by (auto intro: smallest_prime_beyond_smallest)
-    from this `p \<le> n` have *: "smallest_prime_beyond m \<le> n" by (rule order_trans)
+    from this \<open>p \<le> n\<close> have *: "smallest_prime_beyond m \<le> n" by (rule order_trans)
     from assms have ex: "\<exists>p\<le>n. prime p \<and> m \<le> p" by auto
     then have "finite A" by (auto simp add: A_def)
     with * have "Min A = smallest_prime_beyond m"
diff -r 278b65d9339c -r fad653acf58f src/HOL/Number_Theory/Euclidean_Algorithm.thy
--- a/src/HOL/Number_Theory/Euclidean_Algorithm.thy	Fri Jun 19 21:33:03 2015 +0200
+++ b/src/HOL/Number_Theory/Euclidean_Algorithm.thy	Fri Jun 19 21:41:33 2015 +0200
@@ -1,12 +1,12 @@
 (* Author: Manuel Eberl *)
 
-section {* Abstract euclidean algorithm *}
+section \<open>Abstract euclidean algorithm\<close>
 
 theory Euclidean_Algorithm
 imports Complex_Main
 begin
   
-text {*
+text \<open>
   A Euclidean semiring is a semiring upon which the Euclidean algorithm can be
   implemented. It must provide:
   \begin{itemize}
@@ -18,7 +18,7 @@
   \end{itemize}
   The existence of these functions makes it possible to derive gcd and lcm functions 
   for any Euclidean semiring.
-*} 
+\<close> 
 class euclidean_semiring = semiring_div + 
   fixes euclidean_size :: "'a \<Rightarrow> nat"
   fixes normalization_factor :: "'a \<Rightarrow> 'a"
@@ -60,17 +60,17 @@
 proof (cases "a = 0", simp)
   assume "a \<noteq> 0"
   let ?nf = "normalization_factor"
-  from normalization_factor_is_unit[OF `a \<noteq> 0`] have "?nf a \<noteq> 0"
+  from normalization_factor_is_unit[OF \<open>a \<noteq> 0\<close>] have "?nf a \<noteq> 0"
     by auto
   have "?nf (a div ?nf a) * ?nf (?nf a) = ?nf (a div ?nf a * ?nf a)" 
     by (simp add: normalization_factor_mult)
-  also have "a div ?nf a * ?nf a = a" using `a \<noteq> 0`
+  also have "a div ?nf a * ?nf a = a" using \<open>a \<noteq> 0\<close>
     by simp
-  also have "?nf (?nf a) = ?nf a" using `a \<noteq> 0` 
+  also have "?nf (?nf a) = ?nf a" using \<open>a \<noteq> 0\<close> 
     normalization_factor_is_unit normalization_factor_unit by simp
   finally have "normalization_factor (a div normalization_factor a) = 1"  
-    using `?nf a \<noteq> 0` by (metis div_mult_self2_is_id div_self)
-  with `a \<noteq> 0` show ?thesis by simp
+    using \<open>?nf a \<noteq> 0\<close> by (metis div_mult_self2_is_id div_self)
+  with \<open>a \<noteq> 0\<close> show ?thesis by simp
 qed
 
 lemma normalization_0_iff [simp]:
@@ -90,7 +90,7 @@
     apply (subst (asm) unit_eq_div1, blast, subst (asm) unit_div_commute, blast)
     apply (subst div_mult_swap, simp, simp)
     done
-  with `a \<noteq> 0` `b \<noteq> 0` have "\<exists>c. is_unit c \<and> a = c * b"
+  with \<open>a \<noteq> 0\<close> \<open>b \<noteq> 0\<close> have "\<exists>c. is_unit c \<and> a = c * b"
     by (intro exI[of _ "?nf a div ?nf b"], force simp: mult_ac)
   then obtain c where "is_unit c" and "a = c * b" by blast
   then show "associated a b" by (rule is_unit_associatedI) 
@@ -99,7 +99,7 @@
   assume "a \<noteq> 0" "b \<noteq> 0" "associated a b"
   then obtain c where "is_unit c" and "a = c * b" by (blast elim: associated_is_unitE)
   then show "a div ?nf a = b div ?nf b"
-    apply (simp only: `a = c * b` normalization_factor_mult normalization_factor_unit)
+    apply (simp only: \<open>a = c * b\<close> normalization_factor_mult normalization_factor_unit)
     apply (rule div_mult_mult1, force)
     done
   qed
@@ -129,10 +129,10 @@
   assume "b mod a \<noteq> 0"
   from b_dvd_a have b_dvd_mod: "b dvd b mod a" by (simp add: dvd_mod_iff)
   from b_dvd_mod obtain c where "b mod a = b * c" unfolding dvd_def by blast
-    with `b mod a \<noteq> 0` have "c \<noteq> 0" by auto
-  with `b mod a = b * c` have "euclidean_size (b mod a) \<ge> euclidean_size b"
+    with \<open>b mod a \<noteq> 0\<close> have "c \<noteq> 0" by auto
+  with \<open>b mod a = b * c\<close> have "euclidean_size (b mod a) \<ge> euclidean_size b"
       using size_mult_mono by force
-  moreover from `a \<noteq> 0` have "euclidean_size (b mod a) < euclidean_size a"
+  moreover from \<open>a \<noteq> 0\<close> have "euclidean_size (b mod a) < euclidean_size a"
       using mod_size_less by blast
   ultimately show False using size_eq by simp
 qed
@@ -272,7 +272,7 @@
     fix l assume "l dvd a" and "l dvd gcd b c"
     with dvd_trans[OF _ gcd_dvd1] and dvd_trans[OF _ gcd_dvd2]
       have "l dvd b" and "l dvd c" by blast+
-    with `l dvd a` show "l dvd gcd (gcd a b) c"
+    with \<open>l dvd a\<close> show "l dvd gcd (gcd a b) c"
       by (intro gcd_greatest)
   qed
 next
@@ -369,7 +369,7 @@
 proof -
    have "gcd a b dvd a" by (rule gcd_dvd1)
    then obtain c where A: "a = gcd a b * c" unfolding dvd_def by blast
-   with `a \<noteq> 0` show ?thesis by (subst (2) A, intro size_mult_mono) auto
+   with \<open>a \<noteq> 0\<close> show ?thesis by (subst (2) A, intro size_mult_mono) auto
 qed
 
 lemma euclidean_size_gcd_le2 [simp]:
@@ -381,11 +381,11 @@
   shows "euclidean_size (gcd a b) < euclidean_size a"
 proof (rule ccontr)
   assume "\<not>euclidean_size (gcd a b) < euclidean_size a"
-  with `a \<noteq> 0` have "euclidean_size (gcd a b) = euclidean_size a"
+  with \<open>a \<noteq> 0\<close> have "euclidean_size (gcd a b) = euclidean_size a"
     by (intro le_antisym, simp_all)
   with assms have "a dvd gcd a b" by (auto intro: dvd_euclidean_size_eq_imp_dvd)
   hence "a dvd b" using dvd_gcd_D2 by blast
-  with `\<not>a dvd b` show False by contradiction
+  with \<open>\<not>a dvd b\<close> show False by contradiction
 qed
 
 lemma euclidean_size_gcd_less2:
@@ -445,7 +445,7 @@
   let ?nf = "normalization_factor"
   from assms gcd_mult_distrib [of a c b] 
     have A: "a = gcd (a * c) (a * b) * ?nf a" by simp
-  from `c dvd a * b` show ?thesis by (subst A, simp_all add: gcd_greatest)
+  from \<open>c dvd a * b\<close> show ?thesis by (subst A, simp_all add: gcd_greatest)
 qed
 
 lemma coprime_dvd_mult_iff:
@@ -472,7 +472,7 @@
   shows "gcd (k * m) n = gcd m n"
 proof (rule gcd_dvd_antisym)
   have "gcd (gcd (k * m) n) k = gcd (gcd k n) (k * m)" by (simp add: ac_simps)
-  also note `gcd k n = 1`
+  also note \<open>gcd k n = 1\<close>
   finally have "gcd (gcd (k * m) n) k = 1" by simp
   hence "gcd (k * m) n dvd m" by (rule coprime_dvd_mult, simp add: ac_simps)
   moreover have "gcd (k * m) n dvd n" by simp
@@ -488,14 +488,14 @@
   assume ?rhs then show ?lhs unfolding associated_def by (fast intro: mult_dvd_mono)
 next
   assume ?lhs
-  from `?lhs` have "a dvd b * d" unfolding associated_def by (metis dvd_mult_left) 
+  from \<open>?lhs\<close> have "a dvd b * d" unfolding associated_def by (metis dvd_mult_left) 
   hence "a dvd b" by (simp add: coprime_dvd_mult_iff)
-  moreover from `?lhs` have "b dvd a * c" unfolding associated_def by (metis dvd_mult_left) 
+  moreover from \<open>?lhs\<close> have "b dvd a * c" unfolding associated_def by (metis dvd_mult_left) 
   hence "b dvd a" by (simp add: coprime_dvd_mult_iff)
-  moreover from `?lhs` have "c dvd d * b" 
+  moreover from \<open>?lhs\<close> have "c dvd d * b" 
     unfolding associated_def by (auto dest: dvd_mult_right simp add: ac_simps)
   hence "c dvd d" by (simp add: coprime_dvd_mult_iff gcd.commute)
-  moreover from `?lhs` have "d dvd c * a"
+  moreover from \<open>?lhs\<close> have "d dvd c * a"
     unfolding associated_def by (auto dest: dvd_mult_right simp add: ac_simps)
   hence "d dvd c" by (simp add: coprime_dvd_mult_iff gcd.commute)
   ultimately show ?rhs unfolding associated_def by simp
@@ -536,7 +536,7 @@
   moreover from nz have "d \<noteq> 0" by simp
   with div_mult_self1_is_id have "d * (l * u) div d = l * u" . 
   ultimately have "1 = l * u"
-    using `d \<noteq> 0` by simp
+    using \<open>d \<noteq> 0\<close> by simp
   then show "l dvd 1" ..
 qed
 
@@ -555,7 +555,7 @@
 proof (rule coprimeI)
   fix l assume "l dvd d" and "l dvd a"
   hence "l dvd a * b" by simp
-  with `l dvd d` and dab show "l dvd 1" by (auto intro: gcd_greatest)
+  with \<open>l dvd d\<close> and dab show "l dvd 1" by (auto intro: gcd_greatest)
 qed
 
 lemma coprime_rmult:
@@ -564,7 +564,7 @@
 proof (rule coprimeI)
   fix l assume "l dvd d" and "l dvd b"
   hence "l dvd a * b" by simp
-  with `l dvd d` and dab show "l dvd 1" by (auto intro: gcd_greatest)
+  with \<open>l dvd d\<close> and dab show "l dvd 1" by (auto intro: gcd_greatest)
 qed
 
 lemma coprime_mul_eq: "gcd d (a * b) = 1 \<longleftrightarrow> gcd d a = 1 \<and> gcd d b = 1"
@@ -655,7 +655,7 @@
   with dc have "a' dvd b*c" using dvd_trans[of a' a "b*c"] by simp
   from dc ab'(1,2) have "a'*?d dvd (b'*?d) * c" by simp
   hence "?d * a' dvd ?d * (b' * c)" by (simp add: mult_ac)
-  with `?d \<noteq> 0` have "a' dvd b' * c" by simp
+  with \<open>?d \<noteq> 0\<close> have "a' dvd b' * c" by simp
   with coprime_dvd_mult[OF ab'(3)] 
     have "a' dvd c" by (subst (asm) ac_simps, blast)
   with ab'(1) have "a = ?d * a' \<and> ?d dvd b \<and> a' dvd c" by (simp add: mult_ac)
@@ -672,8 +672,8 @@
   let ?d = "gcd a b"
   assume "?d \<noteq> 0"
   from n obtain m where m: "n = Suc m" by (cases n, simp_all)
-  from `?d \<noteq> 0` have zn: "?d ^ n \<noteq> 0" by (rule power_not_zero)
-  from gcd_coprime_exists[OF `?d \<noteq> 0`]
+  from \<open>?d \<noteq> 0\<close> have zn: "?d ^ n \<noteq> 0" by (rule power_not_zero)
+  from gcd_coprime_exists[OF \<open>?d \<noteq> 0\<close>]
     obtain a' b' where ab': "a = a' * ?d" "b = b' * ?d" "gcd a' b' = 1"
     by blast
   from ab have "(a' * ?d) ^ n dvd (b' * ?d) ^ n"
@@ -755,7 +755,7 @@
   hence "gcd a b \<noteq> 0" by simp
   from lcm_gcd have "lcm a b * gcd a b = gcd a b * (a * b div (?nf (a*b) * gcd a b))" 
     by (simp add: mult_ac)
-  also from `a * b \<noteq> 0` have "... = a * b div ?nf (a*b)"
+  also from \<open>a * b \<noteq> 0\<close> have "... = a * b div ?nf (a*b)"
     by (simp add: div_mult_swap mult.commute)
   finally show ?thesis .
 qed (auto simp add: lcm_gcd)
@@ -766,11 +766,11 @@
   assume "a * b \<noteq> 0"
   hence "gcd a b \<noteq> 0" by simp
   let ?c = "1 div normalization_factor (a * b)"
-  from `a * b \<noteq> 0` have [simp]: "is_unit (normalization_factor (a * b))" by simp
+  from \<open>a * b \<noteq> 0\<close> have [simp]: "is_unit (normalization_factor (a * b))" by simp
   from lcm_gcd_prod[of a b] have "lcm a b * gcd a b = a * ?c * b"
     by (simp add: div_mult_swap unit_div_commute)
   hence "lcm a b * gcd a b div gcd a b = a * ?c * b div gcd a b" by simp
-  with `gcd a b \<noteq> 0` have "lcm a b = a * ?c * b div gcd a b"
+  with \<open>gcd a b \<noteq> 0\<close> have "lcm a b = a * ?c * b div gcd a b"
     by (subst (asm) div_mult_self2_is_id, simp_all)
   also have "... = a * (?c * b div gcd a b)"
     by (metis div_mult_swap gcd_dvd2 mult_assoc)
@@ -785,36 +785,36 @@
   hence "is_unit (?nf k)" by simp
   hence "?nf k \<noteq> 0" by (metis not_is_unit_0)
   assume A: "a dvd k" "b dvd k"
-  hence "gcd a b \<noteq> 0" using `k \<noteq> 0` by auto
+  hence "gcd a b \<noteq> 0" using \<open>k \<noteq> 0\<close> by auto
   from A obtain r s where ar: "k = a * r" and bs: "k = b * s" 
     unfolding dvd_def by blast
-  with `k \<noteq> 0` have "r * s \<noteq> 0"
+  with \<open>k \<noteq> 0\<close> have "r * s \<noteq> 0"
     by auto (drule sym [of 0], simp)
   hence "is_unit (?nf (r * s))" by simp
   let ?c = "?nf k div ?nf (r*s)"
-  from `is_unit (?nf k)` and `is_unit (?nf (r * s))` have "is_unit ?c" by (rule unit_div)
+  from \<open>is_unit (?nf k)\<close> and \<open>is_unit (?nf (r * s))\<close> have "is_unit ?c" by (rule unit_div)
   hence "?c \<noteq> 0" using not_is_unit_0 by fast 
   from ar bs have "k * k * gcd s r = ?nf k * k * gcd (k * s) (k * r)"
     by (subst mult_assoc, subst gcd_mult_distrib[of k s r], simp only: ac_simps)
   also have "... = ?nf k * k * gcd ((r*s) * a) ((r*s) * b)"
-    by (subst (3) `k = a * r`, subst (3) `k = b * s`, simp add: algebra_simps)
-  also have "... = ?c * r*s * k * gcd a b" using `r * s \<noteq> 0`
+    by (subst (3) \<open>k = a * r\<close>, subst (3) \<open>k = b * s\<close>, simp add: algebra_simps)
+  also have "... = ?c * r*s * k * gcd a b" using \<open>r * s \<noteq> 0\<close>
     by (subst gcd_mult_distrib'[symmetric], simp add: algebra_simps unit_simps)
   finally have "(a*r) * (b*s) * gcd s r = ?c * k * r * s * gcd a b"
     by (subst ar[symmetric], subst bs[symmetric], simp add: mult_ac)
   hence "a * b * gcd s r * (r * s) = ?c * k * gcd a b * (r * s)"
     by (simp add: algebra_simps)
-  hence "?c * k * gcd a b = a * b * gcd s r" using `r * s \<noteq> 0`
+  hence "?c * k * gcd a b = a * b * gcd s r" using \<open>r * s \<noteq> 0\<close>
     by (metis div_mult_self2_is_id)
   also have "... = lcm a b * gcd a b * gcd s r * ?nf (a*b)"
     by (subst lcm_gcd_prod[of a b], metis gcd_mult_distrib gcd_mult_distrib') 
   also have "... = lcm a b * gcd s r * ?nf (a*b) * gcd a b"
     by (simp add: algebra_simps)
-  finally have "k * ?c = lcm a b * gcd s r * ?nf (a*b)" using `gcd a b \<noteq> 0`
+  finally have "k * ?c = lcm a b * gcd s r * ?nf (a*b)" using \<open>gcd a b \<noteq> 0\<close>
     by (metis mult.commute div_mult_self2_is_id)
-  hence "k = lcm a b * (gcd s r * ?nf (a*b)) div ?c" using `?c \<noteq> 0`
+  hence "k = lcm a b * (gcd s r * ?nf (a*b)) div ?c" using \<open>?c \<noteq> 0\<close>
     by (metis div_mult_self2_is_id mult_assoc) 
-  also have "... = lcm a b * (gcd s r * ?nf (a*b) div ?c)" using `is_unit ?c`
+  also have "... = lcm a b * (gcd s r * ?nf (a*b) div ?c)" using \<open>is_unit ?c\<close>
     by (simp add: unit_simps)
   finally show ?thesis by (rule dvdI)
 qed simp
@@ -826,7 +826,7 @@
   {
     assume "a \<noteq> 0" "b \<noteq> 0"
     hence "a * b div ?nf (a * b) \<noteq> 0" by (simp add: no_zero_divisors)
-    moreover from `a \<noteq> 0` and `b \<noteq> 0` have "gcd a b \<noteq> 0" by simp
+    moreover from \<open>a \<noteq> 0\<close> and \<open>b \<noteq> 0\<close> have "gcd a b \<noteq> 0" by simp
     ultimately have "lcm a b \<noteq> 0" using lcm_gcd_prod[of a b] by (intro notI, simp)
   } moreover {
     assume "a = 0 \<or> b = 0"
@@ -843,12 +843,12 @@
 proof-
   from assms have "gcd a b \<noteq> 0" by (simp add: lcm_zero)
   let ?c = "normalization_factor (a * b)"
-  from `lcm a b \<noteq> 0` have "?c \<noteq> 0" by (intro notI, simp add: lcm_zero no_zero_divisors)
+  from \<open>lcm a b \<noteq> 0\<close> have "?c \<noteq> 0" by (intro notI, simp add: lcm_zero no_zero_divisors)
   hence "is_unit ?c" by simp
   from lcm_gcd_prod [of a b] have "gcd a b = a * b div ?c div lcm a b"
-    by (subst (2) div_mult_self2_is_id[OF `lcm a b \<noteq> 0`, symmetric], simp add: mult_ac)
-  also from `is_unit ?c` have "... = a * b div (lcm a b * ?c)"
-    by (metis `?c \<noteq> 0` div_mult_mult1 dvd_mult_div_cancel mult_commute normalization_factor_dvd')
+    by (subst (2) div_mult_self2_is_id[OF \<open>lcm a b \<noteq> 0\<close>, symmetric], simp add: mult_ac)
+  also from \<open>is_unit ?c\<close> have "... = a * b div (lcm a b * ?c)"
+    by (metis \<open>?c \<noteq> 0\<close> div_mult_mult1 dvd_mult_div_cancel mult_commute normalization_factor_dvd')
   finally show ?thesis .
 qed
 
@@ -891,11 +891,11 @@
 
     fix l assume "a dvd l" and "lcm b c dvd l"
     have "b dvd lcm b c" by simp
-    from this and `lcm b c dvd l` have "b dvd l" by (rule dvd_trans)
+    from this and \<open>lcm b c dvd l\<close> have "b dvd l" by (rule dvd_trans)
     have "c dvd lcm b c" by simp
-    from this and `lcm b c dvd l` have "c dvd l" by (rule dvd_trans)
-    from `a dvd l` and `b dvd l` have "lcm a b dvd l" by (rule lcm_least)
-    from this and `c dvd l` show "lcm (lcm a b) c dvd l" by (rule lcm_least)
+    from this and \<open>lcm b c dvd l\<close> have "c dvd l" by (rule dvd_trans)
+    from \<open>a dvd l\<close> and \<open>b dvd l\<close> have "lcm a b dvd l" by (rule lcm_least)
+    from this and \<open>c dvd l\<close> show "lcm (lcm a b) c dvd l" by (rule lcm_least)
   qed (simp add: lcm_zero)
 next
   fix a b
@@ -926,7 +926,7 @@
   hence "is_unit (lcm a b)" by (rule lcm_least)
   hence "lcm a b = normalization_factor (lcm a b)"
     by (subst normalization_factor_unit, simp_all)
-  also have "\<dots> = 1" using `is_unit a \<and> is_unit b`
+  also have "\<dots> = 1" using \<open>is_unit a \<and> is_unit b\<close>
     by auto
   finally show "lcm a b = 1" .
 qed
@@ -999,7 +999,7 @@
 proof -
   have "a dvd lcm a b" by (rule lcm_dvd1)
   then obtain c where A: "lcm a b = a * c" unfolding dvd_def by blast
-  with `a \<noteq> 0` and `b \<noteq> 0` have "c \<noteq> 0" by (auto simp: lcm_zero)
+  with \<open>a \<noteq> 0\<close> and \<open>b \<noteq> 0\<close> have "c \<noteq> 0" by (auto simp: lcm_zero)
   then show ?thesis by (subst A, intro size_mult_mono)
 qed
 
@@ -1013,12 +1013,12 @@
 proof (rule ccontr)
   from assms have "a \<noteq> 0" by auto
   assume "\<not>euclidean_size a < euclidean_size (lcm a b)"
-  with `a \<noteq> 0` and `b \<noteq> 0` have "euclidean_size (lcm a b) = euclidean_size a"
+  with \<open>a \<noteq> 0\<close> and \<open>b \<noteq> 0\<close> have "euclidean_size (lcm a b) = euclidean_size a"
     by (intro le_antisym, simp, intro euclidean_size_lcm_le1)
   with assms have "lcm a b dvd a" 
     by (rule_tac dvd_euclidean_size_eq_imp_dvd) (auto simp: lcm_zero)
   hence "b dvd a" by (rule dvd_lcm_D2)
-  with `\<not>b dvd a` show False by contradiction
+  with \<open>\<not>b dvd a\<close> show False by contradiction
 qed
 
 lemma euclidean_size_lcm_less2:
@@ -1101,8 +1101,8 @@
       unfolding l_def by simp_all
     {
       fix l' assume "\<forall>a\<in>A. a dvd l'"
-      with `\<forall>a\<in>A. a dvd l` have "\<forall>a\<in>A. a dvd gcd l l'" by (auto intro: gcd_greatest)
-      moreover from `l \<noteq> 0` have "gcd l l' \<noteq> 0" by simp
+      with \<open>\<forall>a\<in>A. a dvd l\<close> have "\<forall>a\<in>A. a dvd gcd l l'" by (auto intro: gcd_greatest)
+      moreover from \<open>l \<noteq> 0\<close> have "gcd l l' \<noteq> 0" by simp
       ultimately have "\<exists>b. b \<noteq> 0 \<and> (\<forall>a\<in>A. a dvd b) \<and> euclidean_size b = euclidean_size (gcd l l')"
         by (intro exI[of _ "gcd l l'"], auto)
       hence "euclidean_size (gcd l l') \<ge> n" by (subst n_def) (rule Least_le)
@@ -1110,20 +1110,20 @@
       proof -
         have "gcd l l' dvd l" by simp
         then obtain a where "l = gcd l l' * a" unfolding dvd_def by blast
-        with `l \<noteq> 0` have "a \<noteq> 0" by auto
+        with \<open>l \<noteq> 0\<close> have "a \<noteq> 0" by auto
         hence "euclidean_size (gcd l l') \<le> euclidean_size (gcd l l' * a)"
           by (rule size_mult_mono)
-        also have "gcd l l' * a = l" using `l = gcd l l' * a` ..
-        also note `euclidean_size l = n`
+        also have "gcd l l' * a = l" using \<open>l = gcd l l' * a\<close> ..
+        also note \<open>euclidean_size l = n\<close>
         finally show "euclidean_size (gcd l l') \<le> n" .
       qed
       ultimately have "euclidean_size l = euclidean_size (gcd l l')" 
-        by (intro le_antisym, simp_all add: `euclidean_size l = n`)
-      with `l \<noteq> 0` have "l dvd gcd l l'" by (blast intro: dvd_euclidean_size_eq_imp_dvd)
+        by (intro le_antisym, simp_all add: \<open>euclidean_size l = n\<close>)
+      with \<open>l \<noteq> 0\<close> have "l dvd gcd l l'" by (blast intro: dvd_euclidean_size_eq_imp_dvd)
       hence "l dvd l'" by (blast dest: dvd_gcd_D2)
     }
 
-    with `(\<forall>a\<in>A. a dvd l)` and normalization_factor_is_unit[OF `l \<noteq> 0`] and `l \<noteq> 0`
+    with \<open>(\<forall>a\<in>A. a dvd l)\<close> and normalization_factor_is_unit[OF \<open>l \<noteq> 0\<close>] and \<open>l \<noteq> 0\<close>
       have "(\<forall>a\<in>A. a dvd l div normalization_factor l) \<and> 
         (\<forall>l'. (\<forall>a\<in>A. a dvd l') \<longrightarrow> l div normalization_factor l dvd l') \<and>
         normalization_factor (l div normalization_factor l) = 
@@ -1206,7 +1206,7 @@
     hence "l div normalization_factor l \<noteq> 0" by simp
     also from ex have "l div normalization_factor l = Lcm A"
        by (simp only: Lcm_Lcm_eucl Lcm_eucl_def n_def l_def if_True Let_def)
-    finally show False using `Lcm A = 0` by contradiction
+    finally show False using \<open>Lcm A = 0\<close> by contradiction
   qed
 qed (simp only: Lcm_Lcm_eucl Lcm_eucl_def if_False)
 
@@ -1218,13 +1218,13 @@
   moreover {
     assume "0 \<notin> A"
     hence "\<Prod>A \<noteq> 0" 
-      apply (induct rule: finite_induct[OF `finite A`]) 
+      apply (induct rule: finite_induct[OF \<open>finite A\<close>]) 
       apply simp
       apply (subst setprod.insert, assumption, assumption)
       apply (rule no_zero_divisors)
       apply blast+
       done
-    moreover from `finite A` have "\<forall>a\<in>A. a dvd \<Prod>A" by blast
+    moreover from \<open>finite A\<close> have "\<forall>a\<in>A. a dvd \<Prod>A" by blast
     ultimately have "\<exists>l. l \<noteq> 0 \<and> (\<forall>a\<in>A. a dvd l)" by blast
     with Lcm0_iff' have "Lcm A \<noteq> 0" by simp
   }
@@ -1244,13 +1244,13 @@
 proof (rule lcmI)
   fix l assume "a dvd l" and "Lcm A dvd l"
   hence "\<forall>a\<in>A. a dvd l" by (blast intro: dvd_trans dvd_Lcm)
-  with `a dvd l` show "Lcm (insert a A) dvd l" by (force intro: Lcm_dvd)
+  with \<open>a dvd l\<close> show "Lcm (insert a A) dvd l" by (force intro: Lcm_dvd)
 qed (auto intro: Lcm_dvd dvd_Lcm)
  
 lemma Lcm_finite:
   assumes "finite A"
   shows "Lcm A = Finite_Set.fold lcm 1 A"
-  by (induct rule: finite.induct[OF `finite A`])
+  by (induct rule: finite.induct[OF \<open>finite A\<close>])
     (simp_all add: comp_fun_idem.fold_insert_idem[OF comp_fun_idem_lcm])
 
 lemma Lcm_set [code_unfold]:
@@ -1337,13 +1337,13 @@
 proof (rule gcdI)
   fix l assume "l dvd a" and "l dvd Gcd A"
   hence "\<forall>a\<in>A. l dvd a" by (blast intro: dvd_trans Gcd_dvd)
-  with `l dvd a` show "l dvd Gcd (insert a A)" by (force intro: Gcd_dvd)
+  with \<open>l dvd a\<close> show "l dvd Gcd (insert a A)" by (force intro: Gcd_dvd)
 qed auto
 
 lemma Gcd_finite:
   assumes "finite A"
   shows "Gcd A = Finite_Set.fold gcd 0 A"
-  by (induct rule: finite.induct[OF `finite A`])
+  by (induct rule: finite.induct[OF \<open>finite A\<close>])
     (simp_all add: comp_fun_idem.fold_insert_idem[OF comp_fun_idem_gcd])
 
 lemma Gcd_set [code_unfold]:
@@ -1361,10 +1361,10 @@
   
 end
 
-text {*
+text \<open>
   A Euclidean ring is a Euclidean semiring with additive inverses. It provides a 
   few more lemmas; in particular, Bezout's lemma holds for any Euclidean ring.
-*}
+\<close>
 
 class euclidean_ring = euclidean_semiring + idom
 
diff -r 278b65d9339c -r fad653acf58f src/HOL/Number_Theory/Fib.thy
--- a/src/HOL/Number_Theory/Fib.thy	Fri Jun 19 21:33:03 2015 +0200
+++ b/src/HOL/Number_Theory/Fib.thy	Fri Jun 19 21:41:33 2015 +0200
@@ -8,14 +8,14 @@
 Jeremy Avigad.
 *)
 
-section {* Fib *}
+section \<open>Fib\<close>
 
 theory Fib
 imports Main "../GCD" "../Binomial"
 begin
 
 
-subsection {* Fibonacci numbers *}
+subsection \<open>Fibonacci numbers\<close>
 
 fun fib :: "nat \<Rightarrow> nat"
 where
@@ -23,7 +23,7 @@
   | fib1: "fib (Suc 0) = 1"
   | fib2: "fib (Suc (Suc n)) = fib (Suc n) + fib n"
 
-subsection {* Basic Properties *}
+subsection \<open>Basic Properties\<close>
 
 lemma fib_1 [simp]: "fib (1::nat) = 1"
   by (metis One_nat_def fib1)
@@ -41,12 +41,12 @@
 lemma fib_neq_0_nat: "n > 0 \<Longrightarrow> fib n > 0"
   by (induct n rule: fib.induct) (auto simp add: )
 
-subsection {* A Few Elementary Results *}
+subsection \<open>A Few Elementary Results\<close>
 
-text {*
+text \<open>
   \medskip Concrete Mathematics, page 278: Cassini's identity.  The proof is
   much easier using integers, not natural numbers!
-*}
+\<close>
 
 lemma fib_Cassini_int: "int (fib (Suc (Suc n)) * fib n) - int((fib (Suc n))\<^sup>2) = - ((-1)^n)"
   by (induction n rule: fib.induct)  (auto simp add: field_simps power2_eq_square power_add)
@@ -57,7 +57,7 @@
 using fib_Cassini_int [of n] by auto
 
 
-subsection {* Law 6.111 of Concrete Mathematics *}
+subsection \<open>Law 6.111 of Concrete Mathematics\<close>
 
 lemma coprime_fib_Suc_nat: "coprime (fib (n::nat)) (fib (Suc n))"
   apply (induct n rule: fib.induct)
@@ -86,13 +86,13 @@
     case True
     then have "m \<le> n" by auto
     with pos_m have pos_n: "0 < n" by auto
-    with pos_m `m < n` have diff: "n - m < n" by auto
+    with pos_m \<open>m < n\<close> have diff: "n - m < n" by auto
     have "gcd (fib m) (fib (n mod m)) = gcd (fib m) (fib ((n - m) mod m))"
-      by (simp add: mod_if [of n]) (insert `m < n`, auto)
+      by (simp add: mod_if [of n]) (insert \<open>m < n\<close>, auto)
     also have "\<dots> = gcd (fib m)  (fib (n - m))"
       by (simp add: less.hyps diff pos_m)
     also have "\<dots> = gcd (fib m) (fib n)"
-      by (simp add: gcd_fib_diff `m \<le> n`)
+      by (simp add: gcd_fib_diff \<open>m \<le> n\<close>)
     finally show "gcd (fib m) (fib (n mod m)) = gcd (fib m) (fib n)" .
   next
     case False
@@ -102,14 +102,14 @@
 qed
 
 lemma fib_gcd: "fib (gcd m n) = gcd (fib m) (fib n)"
-    -- {* Law 6.111 *}
+    -- \<open>Law 6.111\<close>
   by (induct m n rule: gcd_nat_induct) (simp_all add: gcd_non_0_nat gcd_commute_nat gcd_fib_mod)
 
 theorem fib_mult_eq_setsum_nat:
     "fib (Suc n) * fib n = (\<Sum>k \<in> {..n}. fib k * fib k)"
   by (induct n rule: nat.induct) (auto simp add:  field_simps)
 
-subsection {* Fibonacci and Binomial Coefficients *}
+subsection \<open>Fibonacci and Binomial Coefficients\<close>
 
 lemma setsum_drop_zero: "(\<Sum>k = 0..Suc n. if 0<k then (f (k - 1)) else 0) = (\<Sum>j = 0..n. f j)"
   by (induct n) auto
diff -r 278b65d9339c -r fad653acf58f src/HOL/Number_Theory/Gauss.thy
--- a/src/HOL/Number_Theory/Gauss.thy	Fri Jun 19 21:33:03 2015 +0200
+++ b/src/HOL/Number_Theory/Gauss.thy	Fri Jun 19 21:41:33 2015 +0200
@@ -3,7 +3,7 @@
 Ported by lcp but unfinished
 *)
 
-section {* Gauss' Lemma *}
+section \<open>Gauss' Lemma\<close>
 
 theory Gauss
 imports Residues
@@ -38,7 +38,7 @@
 definition "F = (\<lambda>x. (int p - x)) ` E"
 
 
-subsection {* Basic properties of p *}
+subsection \<open>Basic properties of p\<close>
 
 lemma odd_p: "odd p"
 by (metis p_prime p_ge_2 prime_odd_nat)
@@ -60,7 +60,7 @@
   by (auto simp add: even_iff_mod_2_eq_zero) (metis p_eq2)
 
 
-subsection {* Basic Properties of the Gauss Sets *}
+subsection \<open>Basic Properties of the Gauss Sets\<close>
 
 lemma finite_A: "finite (A)"
 by (auto simp add: A_def)
@@ -208,7 +208,7 @@
   by (metis id_def all_A_relprime setprod_coprime_int)
 
 
-subsection {* Relationships Between Gauss Sets *}
+subsection \<open>Relationships Between Gauss Sets\<close>
 
 lemma StandardRes_inj_on_ResSet: "ResSet m X \<Longrightarrow> (inj_on (\<lambda>b. b mod m) X)"
   by (auto simp add: ResSet_def inj_on_def cong_int_def)
@@ -315,7 +315,7 @@
 qed
 
 
-subsection {* Gauss' Lemma *}
+subsection \<open>Gauss' Lemma\<close>
 
 lemma aux: "setprod id A * (- 1) ^ card E * a ^ card A * (- 1) ^ card E = setprod id A * a ^ card A"
 by (metis (no_types) minus_minus mult.commute mult.left_commute power_minus power_one)
diff -r 278b65d9339c -r fad653acf58f src/HOL/Number_Theory/MiscAlgebra.thy
--- a/src/HOL/Number_Theory/MiscAlgebra.thy	Fri Jun 19 21:33:03 2015 +0200
+++ b/src/HOL/Number_Theory/MiscAlgebra.thy	Fri Jun 19 21:41:33 2015 +0200
@@ -291,7 +291,7 @@
 proof -
   have "(x \<oplus> \<one>) \<otimes> (x \<oplus> \<ominus> \<one>) = x \<otimes> x \<oplus> \<ominus> \<one>"
     by (simp add: ring_simprules)
-  also from `x \<otimes> x = \<one>` have "\<dots> = \<zero>"
+  also from \<open>x \<otimes> x = \<one>\<close> have "\<dots> = \<zero>"
     by (simp add: ring_simprules)
   finally have "(x \<oplus> \<one>) \<otimes> (x \<oplus> \<ominus> \<one>) = \<zero>" .
   then have "(x \<oplus> \<one>) = \<zero> | (x \<oplus> \<ominus> \<one>) = \<zero>"
diff -r 278b65d9339c -r fad653acf58f src/HOL/Number_Theory/Number_Theory.thy
--- a/src/HOL/Number_Theory/Number_Theory.thy	Fri Jun 19 21:33:03 2015 +0200
+++ b/src/HOL/Number_Theory/Number_Theory.thy	Fri Jun 19 21:41:33 2015 +0200
@@ -1,5 +1,5 @@
 
-section {* Comprehensive number theory *}
+section \<open>Comprehensive number theory\<close>
 
 theory Number_Theory
 imports Fib Residues Eratosthenes
diff -r 278b65d9339c -r fad653acf58f src/HOL/Number_Theory/Pocklington.thy
--- a/src/HOL/Number_Theory/Pocklington.thy	Fri Jun 19 21:33:03 2015 +0200
+++ b/src/HOL/Number_Theory/Pocklington.thy	Fri Jun 19 21:41:33 2015 +0200
@@ -2,13 +2,13 @@
     Author:     Amine Chaieb
 *)
 
-section {* Pocklington's Theorem for Primes *}
+section \<open>Pocklington's Theorem for Primes\<close>
 
 theory Pocklington
 imports Residues
 begin
 
-subsection{*Lemmas about previously defined terms*}
+subsection\<open>Lemmas about previously defined terms\<close>
 
 lemma prime: 
   "prime p \<longleftrightarrow> p \<noteq> 0 \<and> p\<noteq>1 \<and> (\<forall>m. 0 < m \<and> m < p \<longrightarrow> coprime p m)"
@@ -52,7 +52,7 @@
 qed
 
 
-subsection{*Some basic theorems about solving congruences*}
+subsection\<open>Some basic theorems about solving congruences\<close>
 
 lemma cong_solve: 
   fixes n::nat assumes an: "coprime a n" shows "\<exists>x. [a * x = b] (mod n)"
@@ -135,7 +135,7 @@
 qed
 
 
-subsection{*Lucas's theorem*}
+subsection\<open>Lucas's theorem\<close>
 
 lemma phi_limit_strong: "phi(n) \<le> n - 1"
 proof -
@@ -291,7 +291,7 @@
 qed
 
 
-subsection{*Definition of the order of a number mod n (0 in non-coprime case)*}
+subsection\<open>Definition of the order of a number mod n (0 in non-coprime case)\<close>
 
 definition "ord n a = (if coprime n a then Least (\<lambda>d. d > 0 \<and> [a ^d = 1] (mod n)) else 0)"
 
@@ -442,7 +442,7 @@
   ultimately show ?thesis by blast
 qed
 
-subsection{*Another trivial primality characterization*}
+subsection\<open>Another trivial primality characterization\<close>
 
 lemma prime_prime_factor:
   "prime n \<longleftrightarrow> n \<noteq> 1 \<and> (\<forall>p. prime p \<and> p dvd n \<longrightarrow> p = n)" 
@@ -530,7 +530,7 @@
 qed
 
 
-subsection{*Pocklington theorem*}
+subsection\<open>Pocklington theorem\<close>
 
 lemma pocklington_lemma:
   assumes n: "n \<ge> 2" and nqr: "n - 1 = q*r" and an: "[a^ (n - 1) = 1] (mod n)"
@@ -666,7 +666,7 @@
 qed
 
 
-subsection{*Prime factorizations*}
+subsection\<open>Prime factorizations\<close>
 
 (* FIXME some overlap with material in UniqueFactorization, class unique_factorization *)
 
diff -r 278b65d9339c -r fad653acf58f src/HOL/Number_Theory/Primes.thy
--- a/src/HOL/Number_Theory/Primes.thy	Fri Jun 19 21:33:03 2015 +0200
+++ b/src/HOL/Number_Theory/Primes.thy	Fri Jun 19 21:41:33 2015 +0200
@@ -25,7 +25,7 @@
 *)
 
 
-section {* Primes *}
+section \<open>Primes\<close>
 
 theory Primes
 imports "~~/src/HOL/GCD" "~~/src/HOL/Binomial"
@@ -40,7 +40,7 @@
 lemmas prime_nat_def = prime_def
 
 
-subsection {* Primes *}
+subsection \<open>Primes\<close>
 
 lemma prime_odd_nat: "prime p \<Longrightarrow> p > 2 \<Longrightarrow> odd p"
   apply (auto simp add: prime_nat_def even_iff_mod_2_eq_zero dvd_eq_mod_eq_0)
@@ -126,7 +126,7 @@
   by (cases n) (auto elim: prime_dvd_power_int)
 
 
-subsubsection {* Make prime naively executable *}
+subsubsection \<open>Make prime naively executable\<close>
 
 lemma zero_not_prime_nat [simp]: "~prime (0::nat)"
   by (simp add: prime_nat_def)
@@ -152,7 +152,7 @@
 lemma two_is_prime_nat [simp]: "prime (2::nat)"
   by simp
 
-text{* A bit of regression testing: *}
+text\<open>A bit of regression testing:\<close>
 
 lemma "prime(97::nat)" by simp
 lemma "prime(997::nat)" by eval
@@ -181,7 +181,7 @@
     nat_dvd_not_less neq0_conv prime_nat_def)
   done
 
-text {* One property of coprimality is easier to prove via prime factors. *}
+text \<open>One property of coprimality is easier to prove via prime factors.\<close>
 
 lemma prime_divprod_pow_nat:
   assumes p: "prime p" and ab: "coprime a b" and pab: "p^n dvd a * b"
@@ -222,7 +222,7 @@
 qed
 
 
-subsection {* Infinitely many primes *}
+subsection \<open>Infinitely many primes\<close>
 
 lemma next_prime_bound: "\<exists>p. prime p \<and> n < p \<and> p <= fact n + 1"
 proof-
@@ -231,18 +231,18 @@
   obtain p where "prime p" and "p dvd fact n + 1" by auto
   then have "p \<le> fact n + 1" apply (intro dvd_imp_le) apply auto done
   { assume "p \<le> n"
-    from `prime p` have "p \<ge> 1"
+    from \<open>prime p\<close> have "p \<ge> 1"
       by (cases p, simp_all)
-    with `p <= n` have "p dvd fact n"
+    with \<open>p <= n\<close> have "p dvd fact n"
       by (intro dvd_fact)
-    with `p dvd fact n + 1` have "p dvd fact n + 1 - fact n"
+    with \<open>p dvd fact n + 1\<close> have "p dvd fact n + 1 - fact n"
       by (rule dvd_diff_nat)
     then have "p dvd 1" by simp
     then have "p <= 1" by auto
-    moreover from `prime p` have "p > 1" by auto
+    moreover from \<open>prime p\<close> have "p > 1" by auto
     ultimately have False by auto}
   then have "n < p" by presburger
-  with `prime p` and `p <= fact n + 1` show ?thesis by auto
+  with \<open>prime p\<close> and \<open>p <= fact n + 1\<close> show ?thesis by auto
 qed
 
 lemma bigger_prime: "\<exists>p. prime p \<and> p > (n::nat)"
@@ -259,9 +259,9 @@
     by auto
 qed
 
-subsection{*Powers of Primes*}
+subsection\<open>Powers of Primes\<close>
 
-text{*Versions for type nat only*}
+text\<open>Versions for type nat only\<close>
 
 lemma prime_product:
   fixes p::nat
@@ -271,7 +271,7 @@
   from assms have
     "1 < p * q" and P: "\<And>m. m dvd p * q \<Longrightarrow> m = 1 \<or> m = p * q"
     unfolding prime_nat_def by auto
-  from `1 < p * q` have "p \<noteq> 0" by (cases p) auto
+  from \<open>1 < p * q\<close> have "p \<noteq> 0" by (cases p) auto
   then have Q: "p = p * q \<longleftrightarrow> q = 1" by auto
   have "p dvd p * q" by simp
   then have "p = 1 \<or> p = p * q" by (rule P)
@@ -370,7 +370,7 @@
   thus "\<exists>i\<le>k. d = p ^ i \<Longrightarrow> d dvd p ^ k" by blast
 qed
 
-subsection {*Chinese Remainder Theorem Variants*}
+subsection \<open>Chinese Remainder Theorem Variants\<close>
 
 lemma bezout_gcd_nat:
   fixes a::nat shows "\<exists>x y. a * x - b * y = gcd a b \<or> b * x - a * y = gcd a b"
@@ -391,7 +391,7 @@
 qed
 
 
-text {* A binary form of the Chinese Remainder Theorem. *}
+text \<open>A binary form of the Chinese Remainder Theorem.\<close>
 
 lemma chinese_remainder:
   fixes a::nat  assumes ab: "coprime a b" and a: "a \<noteq> 0" and b: "b \<noteq> 0"
@@ -411,7 +411,7 @@
   thus ?thesis by blast
 qed
 
-text {* Primality *}
+text \<open>Primality\<close>
 
 lemma coprime_bezout_strong:
   fixes a::nat assumes "coprime a b"  "b \<noteq> 1"
diff -r 278b65d9339c -r fad653acf58f src/HOL/Number_Theory/Residues.thy
--- a/src/HOL/Number_Theory/Residues.thy	Fri Jun 19 21:33:03 2015 +0200
+++ b/src/HOL/Number_Theory/Residues.thy	Fri Jun 19 21:41:33 2015 +0200
@@ -5,7 +5,7 @@
 Euler's theorem and Wilson's theorem.
 *)
 
-section {* Residue rings *}
+section \<open>Residue rings\<close>
 
 theory Residues
 imports UniqueFactorization MiscAlgebra
@@ -248,7 +248,7 @@
 *)
 
 
-subsection{* Euler's theorem *}
+subsection\<open>Euler's theorem\<close>
 
 (* the definition of the phi function *)
 
@@ -276,9 +276,9 @@
       apply (rule cop)
       using * apply auto
       done
-    with `x dvd p` `1 < x` have "False" by auto }
+    with \<open>x dvd p\<close> \<open>1 < x\<close> have "False" by auto }
   then show ?thesis
-    using `2 \<le> p`
+    using \<open>2 \<le> p\<close>
     by (simp add: prime_def)
        (metis One_nat_def dvd_pos_nat nat_dvd_not_less nat_neq_iff not_gr0
               not_numeral_le_zero one_dvd)
@@ -374,7 +374,7 @@
 by (metis int_1 of_nat_power transfer_int_nat_cong zdvd_int)
 
 
-subsection {* Wilson's theorem *}
+subsection \<open>Wilson's theorem\<close>
 
 lemma (in field) inv_pair_lemma: "x : Units R \<Longrightarrow> y : Units R \<Longrightarrow>
     {x, inv x} ~= {y, inv y} \<Longrightarrow> {x, inv x} Int {y, inv y} = {}"
diff -r 278b65d9339c -r fad653acf58f src/HOL/Number_Theory/UniqueFactorization.thy
--- a/src/HOL/Number_Theory/UniqueFactorization.thy	Fri Jun 19 21:33:03 2015 +0200
+++ b/src/HOL/Number_Theory/UniqueFactorization.thy	Fri Jun 19 21:41:33 2015 +0200
@@ -8,7 +8,7 @@
 that, by Jeremy Avigad and David Gray.  
 *)
 
-section {* UniqueFactorization *}
+section \<open>UniqueFactorization\<close>
 
 theory UniqueFactorization
 imports Cong "~~/src/HOL/Library/Multiset"
@@ -34,7 +34,7 @@
 *)
 
 
-subsection {* unique factorization: multiset version *}
+subsection \<open>unique factorization: multiset version\<close>
 
 lemma multiset_prime_factorization_exists [rule_format]: "n > 0 --> 
     (EX M. (ALL (p::nat) : set_mset M. prime p) & n = (PROD i :# M. i))"
@@ -154,7 +154,7 @@
 done
 
 
-subsection {* Prime factors and multiplicity for nats and ints *}
+subsection \<open>Prime factors and multiplicity for nats and ints\<close>
 
 class unique_factorization =
   fixes multiplicity :: "'a \<Rightarrow> 'a \<Rightarrow> nat"
@@ -191,7 +191,7 @@
 end
 
 
-subsection {* Set up transfer *}
+subsection \<open>Set up transfer\<close>
 
 lemma transfer_nat_int_prime_factors: "prime_factors (nat n) = nat ` prime_factors n"
   unfolding prime_factors_int_def
@@ -228,7 +228,7 @@
   transfer_int_nat_multiplicity]
 
 
-subsection {* Properties of prime factors and multiplicity for nats and ints *}
+subsection \<open>Properties of prime factors and multiplicity for nats and ints\<close>
 
 lemma prime_factors_ge_0_int [elim]: "p : prime_factors (n::int) \<Longrightarrow> p >= 0"
   unfolding prime_factors_int_def by auto
@@ -308,7 +308,7 @@
     using assms
     apply (simp add: set_mset_def msetprod_multiplicity)
     done
-  with `f \<in> multiset` have "count (multiset_prime_factorization n) = f"
+  with \<open>f \<in> multiset\<close> have "count (multiset_prime_factorization n) = f"
     by simp
   with S_eq show ?thesis
     by (simp add: set_mset_def multiset_def prime_factors_nat_def multiplicity_nat_def)
@@ -710,7 +710,7 @@
   done
 
 
-subsection {* An application *}
+subsection \<open>An application\<close>
 
 lemma gcd_eq_nat: 
   assumes pos [arith]: "x > 0" "y > 0"