src/HOL/IntDiv.thy
changeset 31998 2c7a24f74db9
parent 31734 a4a79836d07b
child 32010 cb1a1c94b4cd
child 32069 6d28bbd33e2c
     1.1 --- a/src/HOL/IntDiv.thy	Tue Jul 14 10:53:44 2009 +0200
     1.2 +++ b/src/HOL/IntDiv.thy	Tue Jul 14 10:54:04 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_inline]: "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