delegate boundary cases to existing IntInf.pow;
authorwenzelm
Fri Nov 03 19:16:41 2017 +0100 (18 months ago)
changeset 6699622ca0f37f491
parent 66995 9cb263dbb2f7
child 66997 17eb23e43630
delegate boundary cases to existing IntInf.pow;
src/Pure/General/integer.ML
     1.1 --- a/src/Pure/General/integer.ML	Fri Nov 03 17:27:00 2017 +0100
     1.2 +++ b/src/Pure/General/integer.ML	Fri Nov 03 19:16:41 2017 +0100
     1.3 @@ -51,7 +51,7 @@
     1.4            in if r = 0 then l' else l' * l end;
     1.5    in
     1.6      if k < 0
     1.7 -    then error "pow: negative exponent"
     1.8 +    then IntInf.pow (l, k)
     1.9      else pw k l
    1.10    end;
    1.11