diff -r 6108dddad9f0 -r f0e07600de47 src/HOL/Number_Theory/Quadratic_Reciprocity.thy
--- a/src/HOL/Number_Theory/Quadratic_Reciprocity.thy	Tue Jan 17 11:26:21 2017 +0100
+++ b/src/HOL/Number_Theory/Quadratic_Reciprocity.thy	Tue Jan 17 13:59:10 2017 +0100
@@ -4,7 +4,7 @@
 imports Gauss
 begin
 
-text {* The proof is based on Gauss's fifth proof, which can be found at http://www.lehigh.edu/~shw2/q-recip/gauss5.pdf *}
+text \<open>The proof is based on Gauss's fifth proof, which can be found at http://www.lehigh.edu/~shw2/q-recip/gauss5.pdf\<close>
 
 locale QR =
   fixes p :: "nat"