src/HOL/Number_Theory/Residues.thy
changeset 67091 1393c2340eec
parent 67051 e7e54a0b9197
child 67341 df79ef3b3a41
     1.1 --- a/src/HOL/Number_Theory/Residues.thy	Sun Nov 26 13:19:52 2017 +0100
     1.2 +++ b/src/HOL/Number_Theory/Residues.thy	Sun Nov 26 21:08:32 2017 +0100
     1.3 @@ -296,7 +296,7 @@
     1.4    fixes a m :: nat
     1.5    assumes "coprime a m"
     1.6    shows "[a ^ totient m = 1] (mod m)"
     1.7 -proof (cases "m = 0 | m = 1")
     1.8 +proof (cases "m = 0 \<or> m = 1")
     1.9    case True
    1.10    then show ?thesis by auto
    1.11  next