--- a/src/HOL/Library/Efficient_Nat.thy Thu Oct 29 22:16:12 2009 +0100
+++ b/src/HOL/Library/Efficient_Nat.thy Thu Oct 29 22:16:40 2009 +0100
@@ -54,15 +54,15 @@
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 = Divides.divmod"
+ [code del]: "divmod_aux = divmod_nat"
lemma [code]:
- "Divides.divmod n m = (if m = 0 then (0, n) else divmod_aux n m)"
- unfolding divmod_aux_def divmod_div_mod by simp
+ "divmod_nat n m = (if m = 0 then (0, n) else divmod_aux n m)"
+ unfolding divmod_aux_def divmod_nat_div_mod by simp
lemma divmod_aux_code [code]:
"divmod_aux n m = (nat (of_nat n div of_nat m), nat (of_nat n mod of_nat m))"
- unfolding divmod_aux_def divmod_div_mod zdiv_int [symmetric] zmod_int [symmetric] by simp
+ unfolding divmod_aux_def divmod_nat_div_mod zdiv_int [symmetric] zmod_int [symmetric] by simp
lemma eq_nat_code [code]:
"eq_class.eq n m \<longleftrightarrow> eq_class.eq (of_nat n \<Colon> int) (of_nat m)"
--- a/src/HOL/Matrix/ComputeNumeral.thy Thu Oct 29 22:16:12 2009 +0100
+++ b/src/HOL/Matrix/ComputeNumeral.thy Thu Oct 29 22:16:40 2009 +0100
@@ -153,16 +153,16 @@
lemma negateSnd: "negateSnd (q, r) = (q, -r)"
by (simp add: negateSnd_def)
-lemma divmod: "IntDiv.divmod a b = (if 0\<le>a then
+lemma divmod: "divmod_int 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: IntDiv.divmod_def)
+ by (auto simp only: divmod_int_def)
-lemmas compute_div_mod = div_def mod_def divmod adjust negateSnd posDivAlg.simps negDivAlg.simps
+lemmas compute_div_mod = div_int_def mod_int_def divmod adjust negateSnd posDivAlg.simps negDivAlg.simps