| author | haftmann |
| Tue, 30 Jun 2009 14:53:58 +0200 | |
| changeset 31872 | a564aca741f2 |
| parent 30694 | 4b182a031731 |
| child 34051 | 1a82e2e29d67 |
| permissions | -rw-r--r-- |
| 30694 | 1 |
(* Title: HOL/Imperative_HOL/Imperative_HOL_ex.thy |
| 31872 | 2 |
Author: John Matthews, Galois Connections; |
3 |
Alexander Krauss, Lukas Bulwahn & Florian Haftmann, TU Muenchen |
|
| 30694 | 4 |
*) |
5 |
||
| 31872 | 6 |
header {* Monadic imperative HOL with examples *}
|
| 30694 | 7 |
|
8 |
theory Imperative_HOL_ex |
|
9 |
imports Imperative_HOL "ex/Imperative_Quicksort" |
|
10 |
begin |
|
11 |
||
12 |
end |