| changeset 21404 | eb85850d3eb7 |
| parent 19670 | 2e4a143c73c5 |
| child 23894 | 1a4167d761ac |
--- a/src/HOL/NumberTheory/WilsonRuss.thy Fri Nov 17 02:19:55 2006 +0100 +++ b/src/HOL/NumberTheory/WilsonRuss.thy Fri Nov 17 02:20:03 2006 +0100 @@ -16,7 +16,7 @@ subsection {* Definitions and lemmas *} definition - inv :: "int => int => int" + inv :: "int => int => int" where "inv p a = (a^(nat (p - 2))) mod p" consts