removed junk;
authorwenzelm
Mon May 22 14:08:22 2017 +0200 (2017-05-22)
changeset 65899ab7d8c999531
parent 65898 f02a1289e2c6
child 65900 d82d1a2e8a4b
removed junk;
src/HOL/Number_Theory/Residues.thy
     1.1 --- a/src/HOL/Number_Theory/Residues.thy	Mon May 22 11:34:42 2017 +0200
     1.2 +++ b/src/HOL/Number_Theory/Residues.thy	Mon May 22 14:08:22 2017 +0200
     1.3 @@ -57,7 +57,7 @@
     1.4    qed
     1.5    with m_gt_one show ?thesis
     1.6      by (fastforce simp add: R_def residue_ring_def mod_add_right_eq ac_simps  intro!: abelian_groupI)
     1.7 -qed    
     1.8 +qed
     1.9  
    1.10  lemma comm_monoid: "comm_monoid R"
    1.11    unfolding R_def residue_ring_def
    1.12 @@ -247,7 +247,6 @@
    1.13  
    1.14  lemma (in residues) totient_eq:
    1.15    "totient (nat m) = card (Units R)"
    1.16 -  thm R_def
    1.17  proof -
    1.18    have *: "inj_on nat (Units R)"
    1.19      by (rule inj_onI) (auto simp add: res_units_eq)