# HG changeset patch # User Andreas Lochbihler # Date 1408949132 -7200 # Node ID f7be22c6646b5dcb22f182ba92cedf4b64d7b253 # Parent 177eeda93a8cc4c89d59f252e8c10a64b634fbd0# Parent f23045003476f9e43dc469d060e98a5931341032 merged diff -r 177eeda93a8c -r f7be22c6646b src/HOL/Code_Evaluation.thy --- a/src/HOL/Code_Evaluation.thy Fri Aug 22 17:35:48 2014 +0200 +++ b/src/HOL/Code_Evaluation.thy Mon Aug 25 08:45:32 2014 +0200 @@ -128,6 +128,15 @@ constant "term_of \ integer \ term" \ (Eval) "HOLogic.mk'_number/ HOLogic.code'_integerT" | constant "term_of \ String.literal \ term" \ (Eval) "HOLogic.mk'_literal" +declare [[code drop: "term_of :: integer \ _"]] + +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 \ integer))) + (term_of (num_of_integer i))" +by(rule term_of_anything[THEN meta_eq_to_obj_eq]) + code_reserved Eval HOLogic