Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
merged
authorhaftmann
Tue, 24 Mar 2009 09:15:59 +0100
changeset 30695 182fb8d27b48
parent 30693 c672c8162f4b (current diff)
parent 30694 4b182a031731 (diff)
child 30696 5f0919630aaa
child 30698 7b09a2d9bcfc
merged
--- /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
isabelle