src/HOL/Library/Efficient_Nat.thy
changeset 33343 2eb0b672ab40
parent 32657 5f13912245ff
child 33364 2bd12592c5e8
--- 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)"