--- a/src/HOL/Library/EfficientNat.thy Mon Dec 18 08:21:29 2006 +0100
+++ b/src/HOL/Library/EfficientNat.thy Mon Dec 18 08:21:30 2006 +0100
@@ -64,13 +64,13 @@
by (simp add: nat_of_int_def)
lemma [code func]: "Suc n = n + 1"
by simp
-lemma [code, code inline]: "m + n = nat (int m + int n)"
+lemma [code]: "m + n = nat (int m + int n)"
by arith
lemma [code func, code inline]: "m + n = nat_of_int (int m + int n)"
by (simp add: nat_of_int_def)
lemma [code, code inline]: "m - n = nat (int m - int n)"
by arith
-lemma [code, code inline]: "m * n = nat (int m * int n)"
+lemma [code]: "m * n = nat (int m * int n)"
unfolding zmult_int by simp
lemma [code func, code inline]: "m * n = nat_of_int (int m * int n)"
proof -