1.1 --- a/src/Tools/isac/Knowledge/EqSystem.thy	Tue Jul 26 16:50:27 2011 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/EqSystem.thy	Wed Jul 27 09:30:15 2011 +0200
     1.3 @@ -23,31 +23,31 @@
     1.4  						 => bool list"
     1.5                    ("((Script SolveSystemScript (_ _ =))// (_))" 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 -  commute_0_equality:  "(0 = a) = (a = 0)" and
    1.14 +  commute_0_equality:  "(0 = a) = (a = 0)" (*and*)
    1.15  
    1.16    (*WN0510 see simliar rules 'isolate_' 'separate_' (by RL)
    1.17      [bdv_1,bdv_2,bdv_3,bdv_4] work also for 2 and 3 bdvs, ugly !*)
    1.18    separate_bdvs_add:   
    1.19      "[| [] from [bdv_1,bdv_2,bdv_3,bdv_4] occur_exactly_in a |] 
    1.20 -		      			     ==> (a + b = c) = (b = c + -1*a)" and
    1.21 +		      			     ==> (a + b = c) = (b = c + -1*a)" (*and*)
    1.22    separate_bdvs0:
    1.23      "[| some_of [bdv_1,bdv_2,bdv_3,bdv_4] occur_in b; Not (b=!=0)  |] 
    1.24 -		      			     ==> (a = b) = (a + -1*b = 0)" and
    1.25 +		      			     ==> (a = b) = (a + -1*b = 0)" (*and*)
    1.26    separate_bdvs_add1:  
    1.27      "[| some_of [bdv_1,bdv_2,bdv_3,bdv_4] occur_in c |] 
    1.28 -		      			     ==> (a = b + c) = (a + -1*c = b)" and
    1.29 +		      			     ==> (a = b + c) = (a + -1*c = b)" (*and*)
    1.30    separate_bdvs_add2:
    1.31      "[| Not (some_of [bdv_1,bdv_2,bdv_3,bdv_4] occur_in a) |] 
    1.32 -		      			     ==> (a + b = c) = (b = -1*a + c)" and
    1.33 +		      			     ==> (a + b = c) = (b = -1*a + c)" (*and*)
    1.34    separate_bdvs_mult:  
    1.35      "[| [] from [bdv_1,bdv_2,bdv_3,bdv_4] occur_exactly_in a; Not (a=!=0) |] 
    1.36  		      			     ==>(a * b = c) = (b = c / a)" 
    1.37 -axiomatization where (*..if replaced by "and" we get an error in 
    1.38 +axioms(*axiomatization where*) (*..if replaced by "and" we get an error in 
    1.39    ---  rewrite in [EqSystem,normalize,2x2] --- step "--- 3---";*)
    1.40    order_system_NxN:     "[a,b] = [b,a]"
    1.41    (*requires rew_ord for termination, eg. ord_simplify_Integral;