src/HOL/Library/Efficient_Nat.thy

 *)
 
 header {* Implementation of natural numbers by target-language integers *}
 
 theory Efficient_Nat
-imports Plain Code_Index Code_Integer
+imports Code_Index Code_Integer
 begin
 
 text {*
   When generating code for functions on natural numbers, the
   canonical representation using @{term "0::nat"} and

   unfolding of_nat_mult [symmetric] by simp
 
 text {* Specialized @{term "op div \<Colon> nat \<Rightarrow> nat \<Rightarrow> nat"} 
   and @{term "op mod \<Colon> nat \<Rightarrow> nat \<Rightarrow> nat"} operations. *}
 
-definition
-  divmod_aux ::  "nat \<Rightarrow> nat \<Rightarrow> nat \<times> nat"
-where
+definition divmod_aux ::  "nat \<Rightarrow> nat \<Rightarrow> nat \<times> nat" where
   [code del]: "divmod_aux = divmod"
 
 lemma [code]:
   "divmod n m = (if m = 0 then (0, n) else divmod_aux n m)"
   unfolding divmod_aux_def divmod_div_mod by simp