--- a/src/HOL/Library/Code_Index.thy Tue Sep 16 09:21:22 2008 +0200
+++ b/src/HOL/Library/Code_Index.thy Tue Sep 16 09:21:24 2008 +0200
@@ -5,7 +5,7 @@
header {* Type of indices *}
theory Code_Index
-imports Plain "~~/src/HOL/Presburger"
+imports Plain "~~/src/HOL/Code_Eval" "~~/src/HOL/Presburger"
begin
text {*
@@ -234,7 +234,8 @@
text {* Measure function (for termination proofs) *}
-lemma [measure_function]: "is_measure nat_of_index" by (rule is_measure_trivial)
+lemma [measure_function]:
+ "is_measure nat_of_index" by (rule is_measure_trivial)
subsection {* ML interface *}
@@ -278,7 +279,7 @@
unfolding div_mod_index_def by simp
-subsection {* Code serialization *}
+subsection {* Code generator setup *}
text {* Implementation of indices by bounded integers *}
@@ -333,4 +334,12 @@
(OCaml "!((_ : int) < _)")
(Haskell infix 4 "<")
+text {* Evaluation *}
+
+lemma [code func, code func del]:
+ "(Code_Eval.term_of \<Colon> index \<Rightarrow> term) = Code_Eval.term_of" ..
+
+code_const "Code_Eval.term_of \<Colon> index \<Rightarrow> term"
+ (SML "HOLogic.mk'_number/ HOLogic.indexT/ (IntInf.fromInt/ _)")
+
end