src/HOL/Library/Efficient_Nat.thy
 changeset 33343 2eb0b672ab40 parent 32657 5f13912245ff child 33364 2bd12592c5e8
```     1.1 --- a/src/HOL/Library/Efficient_Nat.thy	Thu Oct 29 22:16:12 2009 +0100
1.2 +++ b/src/HOL/Library/Efficient_Nat.thy	Thu Oct 29 22:16:40 2009 +0100
1.3 @@ -54,15 +54,15 @@
1.4    and @{term "op mod \<Colon> nat \<Rightarrow> nat \<Rightarrow> nat"} operations. *}
1.5
1.6  definition divmod_aux ::  "nat \<Rightarrow> nat \<Rightarrow> nat \<times> nat" where
1.7 -  [code del]: "divmod_aux = Divides.divmod"
1.8 +  [code del]: "divmod_aux = divmod_nat"
1.9
1.10  lemma [code]:
1.11 -  "Divides.divmod n m = (if m = 0 then (0, n) else divmod_aux n m)"
1.12 -  unfolding divmod_aux_def divmod_div_mod by simp
1.13 +  "divmod_nat n m = (if m = 0 then (0, n) else divmod_aux n m)"
1.14 +  unfolding divmod_aux_def divmod_nat_div_mod by simp
1.15
1.16  lemma divmod_aux_code [code]:
1.17    "divmod_aux n m = (nat (of_nat n div of_nat m), nat (of_nat n mod of_nat m))"
1.18 -  unfolding divmod_aux_def divmod_div_mod zdiv_int [symmetric] zmod_int [symmetric] by simp
1.19 +  unfolding divmod_aux_def divmod_nat_div_mod zdiv_int [symmetric] zmod_int [symmetric] by simp
1.20
1.21  lemma eq_nat_code [code]:
1.22    "eq_class.eq n m \<longleftrightarrow> eq_class.eq (of_nat n \<Colon> int) (of_nat m)"
```