src/HOL/NumberTheory/Euler.thy

 header {* Euler's criterion *}
 
 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)"
 
 
 subsection {* Property for MultInvPair *}