# HG changeset patch
# User Andreas Lochbihler
# Date 1408711180 -7200
# Node ID f23045003476f9e43dc469d060e98a5931341032
# Parent  e92cdae8b3b5981dc394ccabd9ae4012433719da
add code equation for term_of on integer

diff -r e92cdae8b3b5 -r f23045003476 src/HOL/Code_Evaluation.thy
--- a/src/HOL/Code_Evaluation.thy	Fri Aug 22 12:05:47 2014 +0200
+++ b/src/HOL/Code_Evaluation.thy	Fri Aug 22 14:39:40 2014 +0200
@@ -128,6 +128,15 @@
   constant "term_of \<Colon> integer \<Rightarrow> term" \<rightharpoonup> (Eval) "HOLogic.mk'_number/ HOLogic.code'_integerT"
 | constant "term_of \<Colon> String.literal \<Rightarrow> term" \<rightharpoonup> (Eval) "HOLogic.mk'_literal"
 
+declare [[code drop: "term_of :: integer \<Rightarrow> _"]]
+
+lemma term_of_integer [unfolded typerep_fun_def typerep_num_def typerep_integer_def, code]:
+  "Code_Evaluation.term_of (i :: integer) =
+   Code_Evaluation.App
+    (Code_Evaluation.Const (STR ''Num.numeral_class.numeral'') (TYPEREP(num \<Rightarrow> integer)))
+    (term_of (num_of_integer i))"
+by(rule term_of_anything[THEN meta_eq_to_obj_eq])
+
 code_reserved Eval HOLogic