| changeset 16417 | 9bc16273c2d4 |
| parent 15392 | 290bc97038c7 |
| child 16663 | 13e9c402308b |
--- a/src/HOL/NumberTheory/WilsonRuss.thy Fri Jun 17 11:35:35 2005 +0200 +++ b/src/HOL/NumberTheory/WilsonRuss.thy Fri Jun 17 16:12:49 2005 +0200 @@ -9,7 +9,7 @@ header {* Wilson's Theorem according to Russinoff *} -theory WilsonRuss = EulerFermat: +theory WilsonRuss imports EulerFermat begin text {* Wilson's Theorem following quite closely Russinoff's approach