src/HOL/Imperative_HOL/Array.thy
changeset 36176 3fe7e97ccca8
parent 35846 2ae4b7585501
child 37709 70fafefbcc98
     1.1 --- a/src/HOL/Imperative_HOL/Array.thy	Fri Apr 16 20:56:40 2010 +0200
     1.2 +++ b/src/HOL/Imperative_HOL/Array.thy	Fri Apr 16 21:28:09 2010 +0200
     1.3 @@ -92,7 +92,7 @@
     1.4       return a
     1.5     done)"
     1.6  
     1.7 -hide (open) const new map -- {* avoid clashed with some popular names *}
     1.8 +hide_const (open) new map -- {* avoid clashed with some popular names *}
     1.9  
    1.10  
    1.11  subsection {* Properties *}
    1.12 @@ -115,28 +115,28 @@
    1.13  
    1.14  definition new' where
    1.15    [code del]: "new' = Array.new o Code_Numeral.nat_of"
    1.16 -hide (open) const new'
    1.17 +hide_const (open) new'
    1.18  lemma [code]:
    1.19    "Array.new = Array.new' o Code_Numeral.of_nat"
    1.20    by (simp add: new'_def o_def)
    1.21  
    1.22  definition of_list' where
    1.23    [code del]: "of_list' i xs = Array.of_list (take (Code_Numeral.nat_of i) xs)"
    1.24 -hide (open) const of_list'
    1.25 +hide_const (open) of_list'
    1.26  lemma [code]:
    1.27    "Array.of_list xs = Array.of_list' (Code_Numeral.of_nat (List.length xs)) xs"
    1.28    by (simp add: of_list'_def)
    1.29  
    1.30  definition make' where
    1.31    [code del]: "make' i f = Array.make (Code_Numeral.nat_of i) (f o Code_Numeral.of_nat)"
    1.32 -hide (open) const make'
    1.33 +hide_const (open) make'
    1.34  lemma [code]:
    1.35    "Array.make n f = Array.make' (Code_Numeral.of_nat n) (f o Code_Numeral.nat_of)"
    1.36    by (simp add: make'_def o_def)
    1.37  
    1.38  definition length' where
    1.39    [code del]: "length' = Array.length \<guillemotright>== liftM Code_Numeral.of_nat"
    1.40 -hide (open) const length'
    1.41 +hide_const (open) length'
    1.42  lemma [code]:
    1.43    "Array.length = Array.length' \<guillemotright>== liftM Code_Numeral.nat_of"
    1.44    by (simp add: length'_def monad_simp',
    1.45 @@ -145,14 +145,14 @@
    1.46  
    1.47  definition nth' where
    1.48    [code del]: "nth' a = Array.nth a o Code_Numeral.nat_of"
    1.49 -hide (open) const nth'
    1.50 +hide_const (open) nth'
    1.51  lemma [code]:
    1.52    "Array.nth a n = Array.nth' a (Code_Numeral.of_nat n)"
    1.53    by (simp add: nth'_def)
    1.54  
    1.55  definition upd' where
    1.56    [code del]: "upd' a i x = Array.upd (Code_Numeral.nat_of i) x a \<guillemotright> return ()"
    1.57 -hide (open) const upd'
    1.58 +hide_const (open) upd'
    1.59  lemma [code]:
    1.60    "Array.upd i x a = Array.upd' a (Code_Numeral.of_nat i) x \<guillemotright> return a"
    1.61    by (simp add: upd'_def monad_simp upd_return)