src/HOL/Imperative_HOL/ex/Imperative_Reverse.thy
changeset 37798 0b0570445a2a
parent 37797 96551d6b1414
child 37802 f2e9c104cebd
     1.1 --- a/src/HOL/Imperative_HOL/ex/Imperative_Reverse.thy	Tue Jul 13 12:05:20 2010 +0200
     1.2 +++ b/src/HOL/Imperative_HOL/ex/Imperative_Reverse.thy	Tue Jul 13 12:16:24 2010 +0200
     1.3 @@ -8,14 +8,12 @@
     1.4  imports Imperative_HOL Subarray
     1.5  begin
     1.6  
     1.7 -hide_const (open) swap rev
     1.8 -
     1.9  fun swap :: "'a\<Colon>heap array \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> unit Heap" where
    1.10    "swap a i j = do {
    1.11 -     x \<leftarrow> nth a i;
    1.12 -     y \<leftarrow> nth a j;
    1.13 -     upd i y a;
    1.14 -     upd j x a;
    1.15 +     x \<leftarrow> Array.nth a i;
    1.16 +     y \<leftarrow> Array.nth a j;
    1.17 +     Array.upd i y a;
    1.18 +     Array.upd j x a;
    1.19       return ()
    1.20     }"
    1.21  
    1.22 @@ -26,9 +24,6 @@
    1.23     }
    1.24     else return ())"
    1.25  
    1.26 -notation (output) swap ("swap")
    1.27 -notation (output) rev ("rev")
    1.28 -
    1.29  declare swap.simps [simp del] rev.simps [simp del]
    1.30  
    1.31  lemma swap_pointwise: assumes "crel (swap a i j) h h' r"