1.1 --- a/src/Tools/isac/Knowledge/Integrate.thy	Tue Jul 26 16:50:27 2011 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/Integrate.thy	Wed Jul 27 09:30:15 2011 +0200
     1.3 @@ -26,18 +26,18 @@
     1.4    NamedIntegrationScript :: "[real,real, real=>real,  bool] => bool"
     1.5                    ("((Script NamedIntegrationScript (_ _ _=))// (_))" 9)
     1.6  
     1.7 -axiomatization where
     1.8 +axioms(*axiomatization where*)
     1.9  (*stated as axioms, todo: prove as theorems
    1.10    'bdv' is a constant handled on the meta-level 
    1.11     specifically as a 'bound variable'            *)
    1.12  
    1.13 -  integral_const:    "Not (bdv occurs_in u) ==> Integral u D bdv = u * bdv" and
    1.14 -  integral_var:      "Integral bdv D bdv = bdv ^^^ 2 / 2" and
    1.15 +  integral_const:    "Not (bdv occurs_in u) ==> Integral u D bdv = u * bdv" (*and*)
    1.16 +  integral_var:      "Integral bdv D bdv = bdv ^^^ 2 / 2" (*and*)
    1.17  
    1.18    integral_add:      "Integral (u + v) D bdv =  
    1.19 -		     (Integral u D bdv) + (Integral v D bdv)" and
    1.20 +		     (Integral u D bdv) + (Integral v D bdv)" (*and*)
    1.21    integral_mult:     "[| Not (bdv occurs_in u); bdv occurs_in v |] ==>  
    1.22 -		     Integral (u * v) D bdv = u * (Integral v D bdv)" and
    1.23 +		     Integral (u * v) D bdv = u * (Integral v D bdv)" (*and*)
    1.24  (*WN080222: this goes into sub-terms, too ...
    1.25    call_for_new_c:    "[| Not (matches (u + new_c v) a); Not (a is_f_x) |] ==>  
    1.26  		     a = a + new_c a"