| changeset 34051 | 1a82e2e29d67 |
| parent 31872 | a564aca741f2 |
| child 36098 | 53992c639da5 |
| 34050:3d2acb18f2f2 | 34051:1a82e2e29d67 |
|---|---|
4 *) |
4 *) |
5 |
5 |
6 header {* Monadic imperative HOL with examples *} |
6 header {* Monadic imperative HOL with examples *} |
7 |
7 |
8 theory Imperative_HOL_ex |
8 theory Imperative_HOL_ex |
9 imports Imperative_HOL "ex/Imperative_Quicksort" |
9 imports Imperative_HOL "ex/Imperative_Quicksort" "ex/Imperative_Reverse" "ex/Linked_Lists" |
10 begin |
10 begin |
11 |
11 |
12 end |
12 end |