src/HOL/Old_Number_Theory/Residues.thy
 changeset 61382 efac889fccbc parent 58889 5b7a9633cfa8 child 64267 b9a1486e79be
```--- a/src/HOL/Old_Number_Theory/Residues.thy	Sat Oct 10 16:21:34 2015 +0200
+++ b/src/HOL/Old_Number_Theory/Residues.thy	Sat Oct 10 16:26:23 2015 +0200
@@ -2,15 +2,15 @@
*)

-section {* Residue Sets *}
+section \<open>Residue Sets\<close>

theory Residues
imports Int2
begin

-text {*
+text \<open>
\medskip Define the residue of a set, the standard residue,
-  quadratic residues, and prove some basic properties. *}
+  quadratic residues, and prove some basic properties.\<close>

definition ResSet :: "int => int set => bool"
where "ResSet m X = (\<forall>y1 y2. (y1 \<in> X & y2 \<in> X & [y1 = y2] (mod m) --> y1 = y2))"
@@ -33,7 +33,7 @@
where "SRStar p = {x. (0 < x) & (x < p)}"

-subsection {* Some useful properties of StandardRes *}
+subsection \<open>Some useful properties of StandardRes\<close>

lemma StandardRes_prop1: "[x = StandardRes m x] (mod m)"
by (auto simp add: StandardRes_def zcong_zmod)
@@ -61,7 +61,7 @@
by (auto simp add: StandardRes_def zcong_eq_zdvd_prop dvd_def)

-subsection {* Relations between StandardRes, SRStar, and SR *}
+subsection \<open>Relations between StandardRes, SRStar, and SR\<close>

lemma SRStar_SR_prop: "x \<in> SRStar p ==> x \<in> SR p"
by (auto simp add: SRStar_def SR_def)
@@ -115,7 +115,7 @@
by (auto simp add: SRStar_def bdd_int_set_l_l_finite)

-subsection {* Properties relating ResSets with StandardRes *}
+subsection \<open>Properties relating ResSets with StandardRes\<close>

lemma aux: "x mod m = y mod m ==> [x = y] (mod m)"
apply (subgoal_tac "x = y ==> [x = y](mod m)")
@@ -158,7 +158,7 @@