1.1 --- a/src/Tools/isac/Knowledge/Delete.thy	Tue Sep 28 13:30:29 2010 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/Delete.thy	Fri Oct 01 10:23:38 2010 +0200
     1.3 @@ -12,6 +12,8 @@
     1.4   (*Semiring_Normalization.comm_semiring_1_class.normalizing_semiring_rules(19)*)
     1.5    real_mult_minus1:       "-1 * z = - (z::real)"
     1.6    real_mult_2:            "2 * z = z + (z::real)"
     1.7 +  real_diff_0:		  "0 - x = - (x::real)"
     1.8 +
     1.9  
    1.10  ML {* 
    1.11  (* TODO rebuild fun calc, fun term_of_float,fun var_op_float, fun float_op_var: