changeset 63167 | 0909deb8059b |
parent 58889 | 5b7a9633cfa8 |
--- a/src/HOL/Imperative_HOL/Imperative_HOL.thy Thu May 26 16:57:14 2016 +0200 +++ b/src/HOL/Imperative_HOL/Imperative_HOL.thy Thu May 26 17:51:22 2016 +0200 @@ -2,7 +2,7 @@ Author: John Matthews, Galois Connections; Alexander Krauss, Lukas Bulwahn & Florian Haftmann, TU Muenchen *) -section {* Entry point into monadic imperative HOL *} +section \<open>Entry point into monadic imperative HOL\<close> theory Imperative_HOL imports Array Ref