--- 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]:
--- 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