src/HOL/IntDiv.thy
changeset 32069 6d28bbd33e2c
parent 31998 2c7a24f74db9
child 32075 e8e0fb5da77a
     1.1 --- a/src/HOL/IntDiv.thy	Tue Jul 14 16:27:31 2009 +0200
     1.2 +++ b/src/HOL/IntDiv.thy	Tue Jul 14 16:27:32 2009 +0200
     1.3 @@ -36,7 +36,7 @@
     1.4  
     1.5  text{*algorithm for the general case @{term "b\<noteq>0"}*}
     1.6  definition negateSnd :: "int \<times> int \<Rightarrow> int \<times> int" where
     1.7 -  [code_inline]: "negateSnd = apsnd uminus"
     1.8 +  [code_unfold]: "negateSnd = apsnd uminus"
     1.9  
    1.10  definition divmod :: "int \<Rightarrow> int \<Rightarrow> int \<times> int" where
    1.11      --{*The full division algorithm considers all possible signs for a, b