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