| changeset 64911 | f0e07600de47 |
| parent 64593 | 50c715579715 |
| child 65413 | cb7f9d7d35e6 |
--- 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"