--- a/src/HOL/NumberTheory/Euler.thy Fri Nov 17 02:19:55 2006 +0100
+++ b/src/HOL/NumberTheory/Euler.thy Fri Nov 17 02:20:03 2006 +0100
@@ -8,10 +8,11 @@
theory Euler imports Residues EvenOdd begin
definition
- MultInvPair :: "int => int => int => int set"
+ MultInvPair :: "int => int => int => int set" where
"MultInvPair a p j = {StandardRes p j, StandardRes p (a * (MultInv p j))}"
- SetS :: "int => int => int set set"
+definition
+ SetS :: "int => int => int set set" where
"SetS a p = (MultInvPair a p ` SRStar p)"