src/HOL/Imperative_HOL/ex/Imperative_Reverse.thy
changeset 36176 3fe7e97ccca8
parent 36098 53992c639da5
child 37719 271ecd4fb9f9
     1.1 --- a/src/HOL/Imperative_HOL/ex/Imperative_Reverse.thy	Fri Apr 16 20:56:40 2010 +0200
     1.2 +++ b/src/HOL/Imperative_HOL/ex/Imperative_Reverse.thy	Fri Apr 16 21:28:09 2010 +0200
     1.3 @@ -8,7 +8,7 @@
     1.4  imports "~~/src/HOL/Imperative_HOL/Imperative_HOL" Subarray
     1.5  begin
     1.6  
     1.7 -hide (open) const swap rev
     1.8 +hide_const (open) swap rev
     1.9  
    1.10  fun swap :: "'a\<Colon>heap array \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> unit Heap" where
    1.11    "swap a i j = (do