src/HOL/Old_Number_Theory/Gauss.thy
changeset 61382 efac889fccbc
parent 58889 5b7a9633cfa8
child 63566 e5abbdee461a
     1.1 --- a/src/HOL/Old_Number_Theory/Gauss.thy	Sat Oct 10 16:21:34 2015 +0200
     1.2 +++ b/src/HOL/Old_Number_Theory/Gauss.thy	Sat Oct 10 16:26:23 2015 +0200
     1.3 @@ -2,7 +2,7 @@
     1.4      Authors:    Jeremy Avigad, David Gray, and Adam Kramer
     1.5  *)
     1.6  
     1.7 -section {* Gauss' Lemma *}
     1.8 +section \<open>Gauss' Lemma\<close>
     1.9  
    1.10  theory Gauss
    1.11  imports Euler
    1.12 @@ -26,7 +26,7 @@
    1.13  definition "F = (%x. (p - x)) ` E"
    1.14  
    1.15  
    1.16 -subsection {* Basic properties of p *}
    1.17 +subsection \<open>Basic properties of p\<close>
    1.18  
    1.19  lemma p_odd: "p \<in> zOdd"
    1.20    by (auto simp add: p_prime p_g_2 zprime_zOdd_eq_grt_2)
    1.21 @@ -64,7 +64,7 @@
    1.22    done
    1.23  
    1.24  
    1.25 -subsection {* Basic Properties of the Gauss Sets *}
    1.26 +subsection \<open>Basic Properties of the Gauss Sets\<close>
    1.27  
    1.28  lemma finite_A: "finite (A)"
    1.29  by (auto simp add: A_def)
    1.30 @@ -272,7 +272,7 @@
    1.31  by(rule all_relprime_prod_relprime[OF finite_A all_A_relprime])
    1.32  
    1.33  
    1.34 -subsection {* Relationships Between Gauss Sets *}
    1.35 +subsection \<open>Relationships Between Gauss Sets\<close>
    1.36  
    1.37  lemma B_card_eq_A: "card B = card A"
    1.38    using finite_A by (simp add: finite_A B_def inj_on_xa_A card_image)
    1.39 @@ -434,7 +434,7 @@
    1.40  qed
    1.41  
    1.42  
    1.43 -subsection {* Gauss' Lemma *}
    1.44 +subsection \<open>Gauss' Lemma\<close>
    1.45  
    1.46  lemma aux: "setprod id A * (- 1) ^ card E * a ^ card A * (- 1) ^ card E = setprod id A * a ^ card A"
    1.47    by (auto simp add: finite_E neg_one_special)