src/HOL/Library/Efficient_Nat.thy
changeset 28228 7ebe8dc06cbb
parent 27673 52056ddac194
child 28346 b8390cd56b8f
     1.1 --- a/src/HOL/Library/Efficient_Nat.thy	Tue Sep 16 09:21:22 2008 +0200
     1.2 +++ b/src/HOL/Library/Efficient_Nat.thy	Tue Sep 16 09:21:24 2008 +0200
     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_Integer Code_Index
     1.8 +imports Plain Code_Index Code_Integer
     1.9  begin
    1.10  
    1.11  text {*
    1.12 @@ -424,6 +424,15 @@
    1.13    "op < \<Colon>  nat \<Rightarrow> nat \<Rightarrow> bool"  ("(_ </ _)")
    1.14  
    1.15  
    1.16 +text {* Evaluation *}
    1.17 +
    1.18 +lemma [code func, code func del]:
    1.19 +  "(Code_Eval.term_of \<Colon> nat \<Rightarrow> term) = Code_Eval.term_of" ..
    1.20 +
    1.21 +code_const "Code_Eval.term_of \<Colon> nat \<Rightarrow> term"
    1.22 +  (SML "HOLogic.mk'_number/ HOLogic.natT")
    1.23 +
    1.24 +
    1.25  text {* Module names *}
    1.26  
    1.27  code_modulename SML