--- a/src/HOL/Imperative_HOL/ex/Imperative_Reverse.thy Tue Jul 13 11:50:22 2010 +0200
+++ b/src/HOL/Imperative_HOL/ex/Imperative_Reverse.thy Tue Jul 13 12:00:11 2010 +0200
@@ -11,19 +11,19 @@
hide_const (open) swap rev
fun swap :: "'a\<Colon>heap array \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> unit Heap" where
- "swap a i j = (do
+ "swap a i j = do {
x \<leftarrow> nth a i;
y \<leftarrow> nth a j;
upd i y a;
upd j x a;
return ()
- done)"
+ }"
fun rev :: "'a\<Colon>heap array \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> unit Heap" where
- "rev a i j = (if (i < j) then (do
+ "rev a i j = (if (i < j) then do {
swap a i j;
rev a (i + 1) (j - 1)
- done)
+ }
else return ())"
notation (output) swap ("swap")