src/HOL/Old_Number_Theory/Residues.thy
changeset 61382 efac889fccbc
parent 58889 5b7a9633cfa8
child 64267 b9a1486e79be
     1.1 --- a/src/HOL/Old_Number_Theory/Residues.thy	Sat Oct 10 16:21:34 2015 +0200
     1.2 +++ b/src/HOL/Old_Number_Theory/Residues.thy	Sat Oct 10 16:26:23 2015 +0200
     1.3 @@ -2,15 +2,15 @@
     1.4      Authors:    Jeremy Avigad, David Gray, and Adam Kramer
     1.5  *)
     1.6  
     1.7 -section {* Residue Sets *}
     1.8 +section \<open>Residue Sets\<close>
     1.9  
    1.10  theory Residues
    1.11  imports Int2
    1.12  begin
    1.13  
    1.14 -text {*
    1.15 +text \<open>
    1.16    \medskip Define the residue of a set, the standard residue,
    1.17 -  quadratic residues, and prove some basic properties. *}
    1.18 +  quadratic residues, and prove some basic properties.\<close>
    1.19  
    1.20  definition ResSet :: "int => int set => bool"
    1.21    where "ResSet m X = (\<forall>y1 y2. (y1 \<in> X & y2 \<in> X & [y1 = y2] (mod m) --> y1 = y2))"
    1.22 @@ -33,7 +33,7 @@
    1.23    where "SRStar p = {x. (0 < x) & (x < p)}"
    1.24  
    1.25  
    1.26 -subsection {* Some useful properties of StandardRes *}
    1.27 +subsection \<open>Some useful properties of StandardRes\<close>
    1.28  
    1.29  lemma StandardRes_prop1: "[x = StandardRes m x] (mod m)"
    1.30    by (auto simp add: StandardRes_def zcong_zmod)
    1.31 @@ -61,7 +61,7 @@
    1.32    by (auto simp add: StandardRes_def zcong_eq_zdvd_prop dvd_def) 
    1.33  
    1.34  
    1.35 -subsection {* Relations between StandardRes, SRStar, and SR *}
    1.36 +subsection \<open>Relations between StandardRes, SRStar, and SR\<close>
    1.37  
    1.38  lemma SRStar_SR_prop: "x \<in> SRStar p ==> x \<in> SR p"
    1.39    by (auto simp add: SRStar_def SR_def)
    1.40 @@ -115,7 +115,7 @@
    1.41    by (auto simp add: SRStar_def bdd_int_set_l_l_finite)
    1.42  
    1.43  
    1.44 -subsection {* Properties relating ResSets with StandardRes *}
    1.45 +subsection \<open>Properties relating ResSets with StandardRes\<close>
    1.46  
    1.47  lemma aux: "x mod m = y mod m ==> [x = y] (mod m)"
    1.48    apply (subgoal_tac "x = y ==> [x = y](mod m)")
    1.49 @@ -158,7 +158,7 @@
    1.50    by (auto simp add: ResSet_def)
    1.51  
    1.52  
    1.53 -subsection {* Property for SRStar *}
    1.54 +subsection \<open>Property for SRStar\<close>
    1.55  
    1.56  lemma ResSet_SRStar_prop: "ResSet p (SRStar p)"
    1.57    by (auto simp add: SRStar_def ResSet_def zcong_zless_imp_eq)