src/HOL/Nat.thy
changeset 29668 33ba3faeaa0e
parent 29652 f4c6e546b7fe
parent 29667 53103fc8ffa3
child 29849 a2baf1b221be
child 29852 3d4c46f62937
--- a/src/HOL/Nat.thy	Wed Jan 28 06:03:46 2009 -0800
+++ b/src/HOL/Nat.thy	Wed Jan 28 16:57:12 2009 +0100
@@ -1265,7 +1265,7 @@
 begin
 
 lemma of_nat_diff: "n \<le> m \<Longrightarrow> of_nat (m - n) = of_nat m - of_nat n"
-  by (simp add: compare_rls of_nat_add [symmetric])
+by (simp add: algebra_simps of_nat_add [symmetric])
 
 end