--- a/src/HOL/IntDiv.thy Tue Jul 14 16:27:31 2009 +0200
+++ b/src/HOL/IntDiv.thy Tue Jul 14 16:27:32 2009 +0200
@@ -36,7 +36,7 @@
text{*algorithm for the general case @{term "b\<noteq>0"}*}
definition negateSnd :: "int \<times> int \<Rightarrow> int \<times> int" where
- [code_inline]: "negateSnd = apsnd uminus"
+ [code_unfold]: "negateSnd = apsnd uminus"
definition divmod :: "int \<Rightarrow> int \<Rightarrow> int \<times> int" where
--{*The full division algorithm considers all possible signs for a, b