# HG changeset patch
# User haftmann
# Date 1246366438 -7200
# Node ID a564aca741f2c04ddc569a5e9adb7445c8ce3e97
# Parent  cc14868409143178dd49347614224120654069e6
tuned

diff -r cc1486840914 -r a564aca741f2 src/HOL/Imperative_HOL/Imperative_HOL_ex.thy
--- a/src/HOL/Imperative_HOL/Imperative_HOL_ex.thy	Tue Jun 30 14:53:57 2009 +0200
+++ b/src/HOL/Imperative_HOL/Imperative_HOL_ex.thy	Tue Jun 30 14:53:58 2009 +0200
@@ -1,8 +1,9 @@
 (*  Title:      HOL/Imperative_HOL/Imperative_HOL_ex.thy
-    Author:     John Matthews, Galois Connections; Alexander Krauss, Lukas Bulwahn & Florian Haftmann, TU Muenchen
+    Author:     John Matthews, Galois Connections;
+                Alexander Krauss, Lukas Bulwahn & Florian Haftmann, TU Muenchen
 *)
 
-header {* Mmonadic imperative HOL with examples *}
+header {* Monadic imperative HOL with examples *}
 
 theory Imperative_HOL_ex
 imports Imperative_HOL "ex/Imperative_Quicksort"