src/HOL/Library/Efficient_Nat.thy
changeset 28694 4e9edaef64dc
parent 28683 59c01ec6cb8d
child 28969 4ed63cdda799
     1.1 --- a/src/HOL/Library/Efficient_Nat.thy	Mon Oct 27 16:15:48 2008 +0100
     1.2 +++ b/src/HOL/Library/Efficient_Nat.thy	Mon Oct 27 16:15:49 2008 +0100
     1.3 @@ -6,7 +6,7 @@
     1.4  header {* Implementation of natural numbers by target-language integers *}
     1.5  
     1.6  theory Efficient_Nat
     1.7 -imports Plain Code_Index Code_Integer
     1.8 +imports Code_Index Code_Integer
     1.9  begin
    1.10  
    1.11  text {*
    1.12 @@ -56,9 +56,7 @@
    1.13  text {* Specialized @{term "op div \<Colon> nat \<Rightarrow> nat \<Rightarrow> nat"} 
    1.14    and @{term "op mod \<Colon> nat \<Rightarrow> nat \<Rightarrow> nat"} operations. *}
    1.15  
    1.16 -definition
    1.17 -  divmod_aux ::  "nat \<Rightarrow> nat \<Rightarrow> nat \<times> nat"
    1.18 -where
    1.19 +definition divmod_aux ::  "nat \<Rightarrow> nat \<Rightarrow> nat \<times> nat" where
    1.20    [code del]: "divmod_aux = divmod"
    1.21  
    1.22  lemma [code]: