1.1 --- a/src/Tools/isac/Knowledge/EqSystem.thy	Mon Sep 06 15:53:18 2010 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/EqSystem.thy	Mon Sep 06 16:56:22 2010 +0200
     1.3 @@ -28,32 +28,32 @@
     1.4    'bdv' is a constant handled on the meta-level 
     1.5     specifically as a 'bound variable'            *)
     1.6  
     1.7 -  commute_0_equality  "(0 = a) = (a = 0)"
     1.8 +  commute_0_equality:  "(0 = a) = (a = 0)"
     1.9  
    1.10    (*WN0510 see simliar rules 'isolate_' 'separate_' (by RL)
    1.11      [bdv_1,bdv_2,bdv_3,bdv_4] work also for 2 and 3 bdvs, ugly !*)
    1.12 -  separate_bdvs_add   
    1.13 +  separate_bdvs_add:   
    1.14      "[| [] from_ [bdv_1,bdv_2,bdv_3,bdv_4] occur_exactly_in a |] 
    1.15  		      			     ==> (a + b = c) = (b = c + -1*a)"
    1.16 -  separate_bdvs0
    1.17 +  separate_bdvs0:
    1.18      "[| some_of [bdv_1,bdv_2,bdv_3,bdv_4] occur_in b; Not (b=!=0)  |] 
    1.19  		      			     ==> (a = b) = (a + -1*b = 0)"
    1.20 -  separate_bdvs_add1  
    1.21 +  separate_bdvs_add1:  
    1.22      "[| some_of [bdv_1,bdv_2,bdv_3,bdv_4] occur_in c |] 
    1.23  		      			     ==> (a = b + c) = (a + -1*c = b)"
    1.24 -  separate_bdvs_add2
    1.25 +  separate_bdvs_add2:
    1.26      "[| Not (some_of [bdv_1,bdv_2,bdv_3,bdv_4] occur_in a) |] 
    1.27  		      			     ==> (a + b = c) = (b = -1*a + c)"
    1.28  
    1.29  
    1.30  
    1.31 -  separate_bdvs_mult  
    1.32 +  separate_bdvs_mult:  
    1.33      "[| [] from_ [bdv_1,bdv_2,bdv_3,bdv_4] occur_exactly_in a; Not (a=!=0) |] 
    1.34  		      			     ==>(a * b = c) = (b = c / a)"
    1.35  
    1.36    (*requires rew_ord for termination, eg. ord_simplify_Integral;
    1.37      works for lists of any length, interestingly !?!*)
    1.38 -  order_system_NxN     "[a,b] = [b,a]"
    1.39 +  order_system_NxN:     "[a,b] = [b,a]"
    1.40  
    1.41  ML {*
    1.42  val thy = @{theory};