src/HOL/IntDiv.thy

 by auto
 termination by (relation "measure (\<lambda>(a, b). nat (- a - b))") auto
 
 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
        including the special case @{text "a=0, b<0"} because 
        @{term negDivAlg} requires @{term "a<0"}.*}