author | blanchet |
Fri, 19 Mar 2010 15:07:44 +0100 | |
changeset 35866 | 513074557e06 |
parent 34051 | 1a82e2e29d67 |
child 36098 | 53992c639da5 |
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 |
|
34051
1a82e2e29d67
added Imperative_HOL examples; added tail-recursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
31872
diff
changeset
|
9 |
imports Imperative_HOL "ex/Imperative_Quicksort" "ex/Imperative_Reverse" "ex/Linked_Lists" |
30694 | 10 |
begin |
11 |
||
12 |
end |