slightly tuned
authorhaftmann
Mon Oct 27 16:15:49 2008 +0100 (2008-10-27)
changeset 286944e9edaef64dc
parent 28693 a1294a197d12
child 28695 f7a06d7284c8
slightly tuned
src/HOL/Library/Efficient_Nat.thy
     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]: