diff -r cd7854f2636d -r 02a9b2540eb7 src/Tools/isac/Knowledge/Delete.thy
--- a/src/Tools/isac/Knowledge/Delete.thy	Tue Sep 28 13:30:29 2010 +0200
+++ b/src/Tools/isac/Knowledge/Delete.thy	Fri Oct 01 10:23:38 2010 +0200
@@ -12,6 +12,8 @@
  (*Semiring_Normalization.comm_semiring_1_class.normalizing_semiring_rules(19)*)
   real_mult_minus1:       "-1 * z = - (z::real)"
   real_mult_2:            "2 * z = z + (z::real)"
+  real_diff_0:		  "0 - x = - (x::real)"
+
 
 ML {* 
 (* TODO rebuild fun calc, fun term_of_float,fun var_op_float, fun float_op_var: