changeset 32657 | 5f13912245ff |
parent 31377 | a48f9ef9de15 |
child 34899 | 8674bb6f727b |
--- a/src/HOL/Library/Code_Integer.thy Wed Sep 23 13:42:53 2009 +0200 +++ b/src/HOL/Library/Code_Integer.thy Wed Sep 23 14:00:12 2009 +0200 @@ -100,7 +100,7 @@ text {* Evaluation *} -code_const "Code_Eval.term_of \<Colon> int \<Rightarrow> term" +code_const "Code_Evaluation.term_of \<Colon> int \<Rightarrow> term" (Eval "HOLogic.mk'_number/ HOLogic.intT") end \ No newline at end of file