# HG changeset patch
# User haftmann
# Date 1256851000 -3600
# Node ID 2eb0b672ab4054799868612e8101675b9fa44575
# Parent  df8b5c05546f922c2dc58510aa5ec95eebc9abd2
adjusted to changes in theory Divides

diff -r df8b5c05546f -r 2eb0b672ab40 src/HOL/Library/Efficient_Nat.thy
--- 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)"
diff -r df8b5c05546f -r 2eb0b672ab40 src/HOL/Matrix/ComputeNumeral.thy
--- 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