equal
deleted
inserted
replaced
182 "~~/src/HOL/Algebra/Ring" |
182 "~~/src/HOL/Algebra/Ring" |
183 "~~/src/HOL/Algebra/FiniteProduct" |
183 "~~/src/HOL/Algebra/FiniteProduct" |
184 theories |
184 theories |
185 Pocklington |
185 Pocklington |
186 Number_Theory |
186 Number_Theory |
|
187 files |
|
188 "document/root.tex" |
187 |
189 |
188 session "HOL-Old_Number_Theory" in Old_Number_Theory = HOL + |
190 session "HOL-Old_Number_Theory" in Old_Number_Theory = HOL + |
189 description {* |
191 description {* |
190 Fundamental Theorem of Arithmetic, Chinese Remainder Theorem, Fermat/Euler |
192 Fundamental Theorem of Arithmetic, Chinese Remainder Theorem, Fermat/Euler |
191 Theorem, Wilson's Theorem, Quadratic Reciprocity. |
193 Theorem, Wilson's Theorem, Quadratic Reciprocity. |