diff -r 17db21aa9aed -r 73ee61385493 src/Tools/isac/Knowledge/Integrate.thy
--- a/src/Tools/isac/Knowledge/Integrate.thy	Mon Apr 19 20:44:18 2021 +0200
+++ b/src/Tools/isac/Knowledge/Integrate.thy	Tue Apr 20 16:58:44 2021 +0200
@@ -26,7 +26,7 @@
    specifically as a 'bound variable'            *)
 
   integral_const:    "Not (bdv occurs_in u) ==> Integral u D bdv = u * bdv" and
-  integral_var:      "Integral bdv D bdv = bdv ^^^ 2 / 2" and
+  integral_var:      "Integral bdv D bdv = bdv \<up> 2 / 2" and
 
   integral_add:      "Integral (u + v) D bdv =  
 		     (Integral u D bdv) + (Integral v D bdv)" and
@@ -36,7 +36,7 @@
   call_for_new_c:    "[| Not (matches (u + new_c v) a); Not (a is_f_x) |] ==>  
 		     a = a + new_c a"
 *)
-  integral_pow:      "Integral bdv ^^^ n D bdv = bdv ^^^ (n+1) / (n + 1)"
+  integral_pow:      "Integral bdv \<up> n D bdv = bdv \<up> (n+1) / (n + 1)"
 
 ML \<open>
 val thy = @{theory};