# HG changeset patch
# User haftmann
# Date 1166426490 -3600
# Node ID aa350df2372cb007d2859e0a4f418d8b7f3ce693
# Parent  62d2416728f55d4c0fc28ca83be12f4d4f775944
dropped two inline directives

diff -r 62d2416728f5 -r aa350df2372c src/HOL/Library/EfficientNat.thy
--- 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 -