src/HOL/Old_Number_Theory/Residues.thy
changeset 53077 a1b3784f8129
parent 41541 1fa4725c4656
child 58889 5b7a9633cfa8
     1.1 --- a/src/HOL/Old_Number_Theory/Residues.thy	Sun Aug 18 18:49:45 2013 +0200
     1.2 +++ b/src/HOL/Old_Number_Theory/Residues.thy	Sun Aug 18 19:59:19 2013 +0200
     1.3 @@ -19,7 +19,7 @@
     1.4    where "StandardRes m x = x mod m"
     1.5  
     1.6  definition QuadRes :: "int => int => bool"
     1.7 -  where "QuadRes m x = (\<exists>y. ([(y ^ 2) = x] (mod m)))"
     1.8 +  where "QuadRes m x = (\<exists>y. ([y\<^sup>2 = x] (mod m)))"
     1.9  
    1.10  definition Legendre :: "int => int => int" where
    1.11    "Legendre a p = (if ([a = 0] (mod p)) then 0