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)