1.1 --- a/src/HOL/Library/Efficient_Nat.thy	Wed Jan 28 11:04:45 2009 +0100
     1.2 +++ b/src/HOL/Library/Efficient_Nat.thy	Wed Jan 28 13:36:11 2009 +0100
     1.3 @@ -56,10 +56,10 @@
     1.4    and @{term "op mod \<Colon> nat \<Rightarrow> nat \<Rightarrow> nat"} operations. *}
     1.5  
     1.6  definition divmod_aux ::  "nat \<Rightarrow> nat \<Rightarrow> nat \<times> nat" where
     1.7 -  [code del]: "divmod_aux = divmod"
     1.8 +  [code del]: "divmod_aux = Divides.divmod"
     1.9  
    1.10  lemma [code]:
    1.11 -  "divmod n m = (if m = 0 then (0, n) else divmod_aux n m)"
    1.12 +  "Divides.divmod n m = (if m = 0 then (0, n) else divmod_aux n m)"
    1.13    unfolding divmod_aux_def divmod_div_mod by simp
    1.14  
    1.15  lemma divmod_aux_code [code]:

     2.1 --- a/src/HOL/Tools/ComputeNumeral.thy	Wed Jan 28 11:04:45 2009 +0100
     2.2 +++ b/src/HOL/Tools/ComputeNumeral.thy	Wed Jan 28 13:36:11 2009 +0100
     2.3 @@ -1,5 +1,5 @@
     2.4  theory ComputeNumeral
     2.5 -imports ComputeHOL "~~/src/HOL/Real/Float"
     2.6 +imports ComputeHOL Float
     2.7  begin
     2.8  
     2.9  (* normalization of bit strings *)
    2.10 @@ -151,18 +151,18 @@
    2.11    by (auto simp only: adjust_def)
    2.12  
    2.13  lemma negateSnd: "negateSnd (q, r) = (q, -r)" 
    2.14 -  by (auto simp only: negateSnd_def)
    2.15 +  by (simp add: negateSnd_def)
    2.16  
    2.17 -lemma divAlg: "divAlg (a, b) = (if 0\<le>a then
    2.18 +lemma divmod: "IntDiv.divmod a b = (if 0\<le>a then
    2.19                    if 0\<le>b then posDivAlg a b
    2.20                    else if a=0 then (0, 0)
    2.21                         else negateSnd (negDivAlg (-a) (-b))
    2.22                 else 
    2.23                    if 0<b then negDivAlg a b
    2.24                    else negateSnd (posDivAlg (-a) (-b)))"
    2.25 -  by (auto simp only: divAlg_def)
    2.26 +  by (auto simp only: IntDiv.divmod_def)
    2.27  
    2.28 -lemmas compute_div_mod = div_def mod_def divAlg adjust negateSnd posDivAlg.simps negDivAlg.simps
    2.29 +lemmas compute_div_mod = div_def mod_def divmod adjust negateSnd posDivAlg.simps negDivAlg.simps
    2.30  
    2.31  
    2.32