| changeset 21404 | eb85850d3eb7 |
| parent 20217 | 25b068a99d2b |
| child 22274 | ce1459004c8d |
--- a/src/HOL/NumberTheory/Int2.thy Fri Nov 17 02:19:55 2006 +0100 +++ b/src/HOL/NumberTheory/Int2.thy Fri Nov 17 02:20:03 2006 +0100 @@ -8,7 +8,7 @@ theory Int2 imports Finite2 WilsonRuss begin definition - MultInv :: "int => int => int" + MultInv :: "int => int => int" where "MultInv p x = x ^ nat (p - 2)"