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