1.1 --- a/src/Tools/isac/Knowledge/Integrate.thy	Mon Sep 06 15:53:18 2010 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/Integrate.thy	Mon Sep 06 16:56:22 2010 +0200
     1.3 @@ -31,18 +31,18 @@
     1.4    'bdv' is a constant handled on the meta-level 
     1.5     specifically as a 'bound variable'            *)
     1.6  
     1.7 -  integral_const    "Not (bdv occurs_in u) ==> Integral u D bdv = u * bdv"
     1.8 -  integral_var      "Integral bdv D bdv = bdv ^^^ 2 / 2"
     1.9 +  integral_const:    "Not (bdv occurs_in u) ==> Integral u D bdv = u * bdv"
    1.10 +  integral_var:      "Integral bdv D bdv = bdv ^^^ 2 / 2"
    1.11  
    1.12 -  integral_add      "Integral (u + v) D bdv =  
    1.13 +  integral_add:      "Integral (u + v) D bdv =  
    1.14  		     (Integral u D bdv) + (Integral v D bdv)"
    1.15 -  integral_mult     "[| Not (bdv occurs_in u); bdv occurs_in v |] ==>  
    1.16 +  integral_mult:     "[| Not (bdv occurs_in u); bdv occurs_in v |] ==>  
    1.17  		     Integral (u * v) D bdv = u * (Integral v D bdv)"
    1.18  (*WN080222: this goes into sub-terms, too ...
    1.19 -  call_for_new_c    "[| Not (matches (u + new_c v) a); Not (a is_f_x) |] ==>  
    1.20 +  call_for_new_c:    "[| Not (matches (u + new_c v) a); Not (a is_f_x) |] ==>  
    1.21  		     a = a + new_c a"
    1.22  *)
    1.23 -  integral_pow      "Integral bdv ^^^ n D bdv = bdv ^^^ (n+1) / (n + 1)"
    1.24 +  integral_pow:      "Integral bdv ^^^ n D bdv = bdv ^^^ (n+1) / (n + 1)"
    1.25  
    1.26  ML {*
    1.27  val thy = @{theory};