| changeset 63537 | 831816778409 |
| parent 63534 | 523b488b15c9 |
| child 63633 | 2accfb71e33b |
--- a/src/HOL/Number_Theory/Residues.thy Fri Jul 22 15:39:32 2016 +0200 +++ b/src/HOL/Number_Theory/Residues.thy Fri Jul 22 17:35:54 2016 +0200 @@ -8,7 +8,7 @@ section \<open>Residue rings\<close> theory Residues -imports UniqueFactorization MiscAlgebra +imports Cong MiscAlgebra begin subsection \<open>A locale for residue rings\<close>