src/HOL/Imperative_HOL/ex/Imperative_Reverse.thy
changeset 37796 08bd610b2583
parent 37771 1bec64044b5e
child 37797 96551d6b1414
     1.1 --- a/src/HOL/Imperative_HOL/ex/Imperative_Reverse.thy	Tue Jul 13 11:38:04 2010 +0200
     1.2 +++ b/src/HOL/Imperative_HOL/ex/Imperative_Reverse.thy	Tue Jul 13 12:01:34 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     done)"
    1.21