equal
deleted
inserted
replaced
6 |
6 |
7 theory Imperative_Reverse |
7 theory Imperative_Reverse |
8 imports "~~/src/HOL/Imperative_HOL/Imperative_HOL" Subarray |
8 imports "~~/src/HOL/Imperative_HOL/Imperative_HOL" Subarray |
9 begin |
9 begin |
10 |
10 |
11 hide (open) const swap rev |
11 hide_const (open) swap rev |
12 |
12 |
13 fun swap :: "'a\<Colon>heap array \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> unit Heap" where |
13 fun swap :: "'a\<Colon>heap array \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> unit Heap" where |
14 "swap a i j = (do |
14 "swap a i j = (do |
15 x \<leftarrow> nth a i; |
15 x \<leftarrow> nth a i; |
16 y \<leftarrow> nth a j; |
16 y \<leftarrow> nth a j; |