changeset 62002 | f1599e98c4d0 |
parent 61032 | b57df8eecad6 |
child 62008 | cbedaddc9351 |
--- a/src/HOL/HOLCF/IOA/Storage/Spec.thy Wed Dec 30 21:56:12 2015 +0100 +++ b/src/HOL/HOLCF/IOA/Storage/Spec.thy Wed Dec 30 21:57:52 2015 +0100 @@ -2,7 +2,7 @@ Author: Olaf Müller *) -section {* The specification of a memory *} +section \<open>The specification of a memory\<close> theory Spec imports "~~/src/HOL/HOLCF/IOA/meta_theory/IOA" Action