1.1 --- a/src/Tools/isac/Knowledge/Poly.thy	Mon Dec 07 14:10:59 2015 +0100
     1.2 +++ b/src/Tools/isac/Knowledge/Poly.thy	Mon Dec 07 15:37:09 2015 +0100
     1.3 @@ -42,7 +42,7 @@
     1.4    realpow_multI:           "(r * s) ^^^ n = r ^^^ n * s ^^^ n"  and
     1.5    realpow_multI_poly:      "[| r is_polyexp; s is_polyexp |] ==>
     1.6  			      (r * s) ^^^ n = r ^^^ n * s ^^^ n"  and
     1.7 -  realpow_minus_oneI:      "-1 ^^^ (2 * n) = 1"  and 
     1.8 +  realpow_minus_oneI:      "(- 1) ^^^ (2 * n) = 1"  and 
     1.9  
    1.10    realpow_twoI:            "r ^^^ 2 = r * r" and
    1.11    realpow_twoI_assoc_l:	  "r * (r * s) = r ^^^ 2 * s" and