diff -r a34d89ce6097 -r 6616e6c53d48 src/ZF/ArithSimp.thy
--- a/src/ZF/ArithSimp.thy	Mon May 26 18:36:15 2003 +0200
+++ b/src/ZF/ArithSimp.thy	Tue May 27 11:39:03 2003 +0200
@@ -12,7 +12,7 @@
 
 subsection{*Difference*}
 
-lemma diff_self_eq_0: "m #- m = 0"
+lemma diff_self_eq_0 [simp]: "m #- m = 0"
 apply (subgoal_tac "natify (m) #- natify (m) = 0")
 apply (rule_tac [2] natify_in_nat [THEN nat_induct], auto)
 done