# HG changeset patch
# User haftmann
# Date 1233146171 -3600
# Node ID 881f328dfbb35614643408c743bf88ceb055283d
# Parent  bd6fb191c00eb6104a5e37bbcce18d3fe25339f2
slightly adapted towards more uniformity with div/mod on nat

diff -r bd6fb191c00e -r 881f328dfbb3 src/HOL/Library/Efficient_Nat.thy
--- a/src/HOL/Library/Efficient_Nat.thy	Wed Jan 28 11:04:45 2009 +0100
+++ b/src/HOL/Library/Efficient_Nat.thy	Wed Jan 28 13:36:11 2009 +0100
@@ -56,10 +56,10 @@
   and @{term "op mod \<Colon> nat \<Rightarrow> nat \<Rightarrow> nat"} operations. *}
 
 definition divmod_aux ::  "nat \<Rightarrow> nat \<Rightarrow> nat \<times> nat" where
-  [code del]: "divmod_aux = divmod"
+  [code del]: "divmod_aux = Divides.divmod"
 
 lemma [code]:
-  "divmod n m = (if m = 0 then (0, n) else divmod_aux n m)"
+  "Divides.divmod n m = (if m = 0 then (0, n) else divmod_aux n m)"
   unfolding divmod_aux_def divmod_div_mod by simp
 
 lemma divmod_aux_code [code]:
diff -r bd6fb191c00e -r 881f328dfbb3 src/HOL/Tools/ComputeNumeral.thy
--- a/src/HOL/Tools/ComputeNumeral.thy	Wed Jan 28 11:04:45 2009 +0100
+++ b/src/HOL/Tools/ComputeNumeral.thy	Wed Jan 28 13:36:11 2009 +0100
@@ -1,5 +1,5 @@
 theory ComputeNumeral
-imports ComputeHOL "~~/src/HOL/Real/Float"
+imports ComputeHOL Float
 begin
 
 (* normalization of bit strings *)
@@ -151,18 +151,18 @@
   by (auto simp only: adjust_def)
 
 lemma negateSnd: "negateSnd (q, r) = (q, -r)" 
-  by (auto simp only: negateSnd_def)
+  by (simp add: negateSnd_def)
 
-lemma divAlg: "divAlg (a, b) = (if 0\<le>a then
+lemma divmod: "IntDiv.divmod a b = (if 0\<le>a then
                   if 0\<le>b then posDivAlg a b
                   else if a=0 then (0, 0)
                        else negateSnd (negDivAlg (-a) (-b))
                else 
                   if 0<b then negDivAlg a b
                   else negateSnd (posDivAlg (-a) (-b)))"
-  by (auto simp only: divAlg_def)
+  by (auto simp only: IntDiv.divmod_def)
 
-lemmas compute_div_mod = div_def mod_def divAlg adjust negateSnd posDivAlg.simps negDivAlg.simps
+lemmas compute_div_mod = div_def mod_def divmod adjust negateSnd posDivAlg.simps negDivAlg.simps