# HG changeset patch
# User haftmann
# Date 1193203193 -7200
# Node ID 0fcb4775cbfbd69ab180dace61aa1f5917610400
# Parent  f737a88a3248fc0cfb70125ebd71ea4a4c8f5e94
dropped superfluous inlining rule

diff -r f737a88a3248 -r 0fcb4775cbfb src/HOL/IntDef.thy
--- a/src/HOL/IntDef.thy	Wed Oct 24 07:19:52 2007 +0200
+++ b/src/HOL/IntDef.thy	Wed Oct 24 07:19:53 2007 +0200
@@ -384,7 +384,7 @@
 definition
   neg  :: "'a\<Colon>ordered_idom \<Rightarrow> bool"
 where
-  [code inline]: "neg Z \<longleftrightarrow> Z < 0"
+  "neg Z \<longleftrightarrow> Z < 0"
 
 definition (*for simplifying equalities*)
   iszero :: "'a\<Colon>semiring_1 \<Rightarrow> bool"