# HG changeset patch
# User haftmann
# Date 1237882559 -3600
# Node ID 182fb8d27b48656f56083e85ca27fa44d4354033
# Parent  c672c8162f4b59c146fa4af5ede72edba141dfa9# Parent  4b182a031731fc2689e39e68428eef7a536dc924
merged

diff -r c672c8162f4b -r 182fb8d27b48 src/HOL/Imperative_HOL/Imperative_HOL_ex.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Imperative_HOL/Imperative_HOL_ex.thy	Tue Mar 24 09:15:59 2009 +0100
@@ -0,0 +1,11 @@
+(*  Title:      HOL/Imperative_HOL/Imperative_HOL_ex.thy
+    Author:     John Matthews, Galois Connections; Alexander Krauss, Lukas Bulwahn & Florian Haftmann, TU Muenchen
+*)
+
+header {* Mmonadic imperative HOL with examples *}
+
+theory Imperative_HOL_ex
+imports Imperative_HOL "ex/Imperative_Quicksort"
+begin
+
+end