--- 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"