| changeset 35848 | 5443079512ea |
| parent 32946 | 22664da2923b |
| child 35849 | b5522b51cb1e |
--- a/src/HOL/Algebra/Exponent.thy Sun Mar 21 15:57:40 2010 +0100 +++ b/src/HOL/Algebra/Exponent.thy Sun Mar 21 16:51:37 2010 +0100 @@ -12,8 +12,9 @@ subsection {*The Combinatorial Argument Underlying the First Sylow Theorem*} -definition exponent :: "nat => nat => nat" where -"exponent p s == if prime p then (GREATEST r. p^r dvd s) else 0" +definition + exponent :: "nat => nat => nat" + where "exponent p s = (if prime p then (GREATEST r. p^r dvd s) else 0)" text{*Prime Theorems*}