| changeset 16417 | 9bc16273c2d4 |
| parent 14889 | d7711d6b9014 |
| child 16663 | 13e9c402308b |
--- a/src/HOL/Algebra/Exponent.thy Fri Jun 17 11:35:35 2005 +0200 +++ b/src/HOL/Algebra/Exponent.thy Fri Jun 17 16:12:49 2005 +0200 @@ -7,7 +7,7 @@ header{*The Combinatorial Argument Underlying the First Sylow Theorem*} -theory Exponent = Main + Primes: +theory Exponent imports Main Primes begin constdefs exponent :: "[nat, nat] => nat"