src/HOL/Code_Numeral.thy
changeset 36176 3fe7e97ccca8
parent 36049 0ce5b7a5c2fd
child 37947 844977c7abeb
     1.1 --- a/src/HOL/Code_Numeral.thy	Fri Apr 16 20:56:40 2010 +0200
     1.2 +++ b/src/HOL/Code_Numeral.thy	Fri Apr 16 21:28:09 2010 +0200
     1.3 @@ -278,7 +278,7 @@
     1.4    then show ?thesis by (auto simp add: int_of_def mult_ac)
     1.5  qed
     1.6  
     1.7 -hide (open) const of_nat nat_of int_of
     1.8 +hide_const (open) of_nat nat_of int_of
     1.9  
    1.10  subsubsection {* Lazy Evaluation of an indexed function *}
    1.11  
    1.12 @@ -289,7 +289,7 @@
    1.13  
    1.14  termination by (relation "measure (%(f, n, m). Code_Numeral.nat_of (m + 1 - n))") auto
    1.15  
    1.16 -hide (open) const iterate_upto
    1.17 +hide_const (open) iterate_upto
    1.18  
    1.19  subsection {* Code generator setup *}
    1.20