1.1 --- a/src/Tools/isac/Knowledge/Integrate.thy	Mon Apr 19 20:44:18 2021 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/Integrate.thy	Tue Apr 20 16:58:44 2021 +0200
     1.3 @@ -26,7 +26,7 @@
     1.4     specifically as a 'bound variable'            *)
     1.5  
     1.6    integral_const:    "Not (bdv occurs_in u) ==> Integral u D bdv = u * bdv" and
     1.7 -  integral_var:      "Integral bdv D bdv = bdv ^^^ 2 / 2" and
     1.8 +  integral_var:      "Integral bdv D bdv = bdv \<up> 2 / 2" and
     1.9  
    1.10    integral_add:      "Integral (u + v) D bdv =  
    1.11  		     (Integral u D bdv) + (Integral v D bdv)" and
    1.12 @@ -36,7 +36,7 @@
    1.13    call_for_new_c:    "[| Not (matches (u + new_c v) a); Not (a is_f_x) |] ==>  
    1.14  		     a = a + new_c a"
    1.15  *)
    1.16 -  integral_pow:      "Integral bdv ^^^ n D bdv = bdv ^^^ (n+1) / (n + 1)"
    1.17 +  integral_pow:      "Integral bdv \<up> n D bdv = bdv \<up> (n+1) / (n + 1)"
    1.18  
    1.19  ML \<open>
    1.20  val thy = @{theory};