1.1 --- a/src/Tools/isac/Knowledge/Poly.thy	Sat Aug 24 12:31:48 2019 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/Poly.thy	Sat Aug 24 12:59:39 2019 +0200
     1.3 @@ -78,6 +78,7 @@
     1.4    realpow_multI_poly:      "[| r is_polyexp; s is_polyexp |] ==>
     1.5  			      (r * s) ^^^ n = r ^^^ n * s ^^^ n"  and
     1.6    realpow_minus_oneI:      "(- 1) ^^^ (2 * n) = 1"  and 
     1.7 +  real_diff_0:		         "0 - x = - (x::real)" and
     1.8  
     1.9    realpow_twoI:            "r ^^^ 2 = r * r" and
    1.10    realpow_twoI_assoc_l:	  "r * (r * s) = r ^^^ 2 * s" and