author | haftmann |
Tue, 13 Jul 2010 16:00:56 +0200 | |
changeset 37804 | 0145e59c1f6c |
parent 37771 | 1bec64044b5e |
child 37826 | 4c0a5e35931a |
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 |
|
37771
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
36098
diff
changeset
|
9 |
imports Imperative_HOL |
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
36098
diff
changeset
|
10 |
"ex/Imperative_Quicksort" "ex/Imperative_Reverse" "ex/Linked_Lists" "ex/SatChecker" |
30694 | 11 |
begin |
12 |
||
13 |
end |