1.1 --- a/src/Tools/isac/Knowledge/Rational.thy	Mon Apr 19 20:44:18 2021 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/Rational.thy	Tue Apr 20 16:58:44 2021 +0200
     1.3 @@ -98,7 +98,7 @@
     1.4    real_divide_divide1_mg:  "y ~= 0 ==> (u / v) / (y / z) = (u * z) / (y * v)" and
     1.5  (*real_divide_divide2_eq:  "x / y / z = x / (y * z)"..Isa02*)
     1.6  			  
     1.7 -  rat_power:               "(a / b)^^^n = (a^^^n) / (b^^^n)" and
     1.8 +  rat_power:               "(a / b) \<up> n = (a \<up> n) / (b \<up> n)" and
     1.9  
    1.10    rat_add:         "[| a is_const; b is_const; c is_const; d is_const |] ==> 
    1.11  	           a / c + b / d = (a * d + b * c) / (c * d)" and