| changeset 14046 | 6616e6c53d48 |
| parent 13784 | b9f6154427a4 |
| child 14055 | a3f592e3f4bd |
--- 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