corrected representation for code_numeral numerals
authorhaftmann
Thu Dec 02 14:34:38 2010 +0100 (2010-12-02)
changeset 408843113fd4810bd
parent 40883 b37dca06477f
child 40885 da4bdafeef7c
corrected representation for code_numeral numerals
src/HOL/Code_Evaluation.thy
     1.1 --- a/src/HOL/Code_Evaluation.thy	Thu Dec 02 13:53:36 2010 +0100
     1.2 +++ b/src/HOL/Code_Evaluation.thy	Thu Dec 02 14:34:38 2010 +0100
     1.3 @@ -153,7 +153,7 @@
     1.4    by (simp only: term_of_anything)
     1.5  
     1.6  lemma (in term_syntax) term_of_code_numeral_code [code]:
     1.7 -  "term_of (k::code_numeral) = termify (number_of :: int \<Rightarrow> code_numeral) <\<cdot>> term_of_num (2::code_numeral) k"
     1.8 +  "term_of (k::code_numeral) = termify (number_of :: int \<Rightarrow> code_numeral) <\<cdot>> term_of_num_semiring (2::code_numeral) k"
     1.9    by (simp only: term_of_anything)
    1.10  
    1.11  definition term_of_num_ring :: "'a\<Colon>ring_div \<Rightarrow> 'a \<Rightarrow> term" where