| changeset 36098 | 53992c639da5 |
| parent 34051 | 1a82e2e29d67 |
| child 36176 | 3fe7e97ccca8 |
| 36097:32383448c01b | 36098:53992c639da5 |
|---|---|
1 (* Title: HOL/Imperative_HOL/ex/Imperative_Reverse.thy |
|
2 Author: Lukas Bulwahn, TU Muenchen |
|
3 *) |
|
4 |
|
5 header {* An imperative in-place reversal on arrays *} |
|
6 |
|
1 theory Imperative_Reverse |
7 theory Imperative_Reverse |
2 imports "~~/src/HOL/Imperative_HOL/Imperative_HOL" Subarray |
8 imports "~~/src/HOL/Imperative_HOL/Imperative_HOL" Subarray |
3 begin |
9 begin |
4 |
10 |
5 hide (open) const swap rev |
11 hide (open) const swap rev |