src/HOL/Old_Number_Theory/Quadratic_Reciprocity.thy
changeset 61382 efac889fccbc
parent 58889 5b7a9633cfa8
child 61609 77b453bd616f
     1.1 --- a/src/HOL/Old_Number_Theory/Quadratic_Reciprocity.thy	Sat Oct 10 16:21:34 2015 +0200
     1.2 +++ b/src/HOL/Old_Number_Theory/Quadratic_Reciprocity.thy	Sat Oct 10 16:26:23 2015 +0200
     1.3 @@ -2,16 +2,16 @@
     1.4      Authors:    Jeremy Avigad, David Gray, and Adam Kramer
     1.5  *)
     1.6  
     1.7 -section {* The law of Quadratic reciprocity *}
     1.8 +section \<open>The law of Quadratic reciprocity\<close>
     1.9  
    1.10  theory Quadratic_Reciprocity
    1.11  imports Gauss
    1.12  begin
    1.13  
    1.14 -text {*
    1.15 +text \<open>
    1.16    Lemmas leading up to the proof of theorem 3.3 in Niven and
    1.17    Zuckerman's presentation.
    1.18 -*}
    1.19 +\<close>
    1.20  
    1.21  context GAUSS
    1.22  begin
    1.23 @@ -153,7 +153,7 @@
    1.24    done
    1.25  
    1.26  
    1.27 -subsection {* Stuff about S, S1 and S2 *}
    1.28 +subsection \<open>Stuff about S, S1 and S2\<close>
    1.29  
    1.30  locale QRTEMP =
    1.31    fixes p     :: "int"