diff -r 5906162c8dd4 -r db8f94656024 src/HOL/Hoare/HeapSyntaxAbort.thy --- a/src/HOL/Hoare/HeapSyntaxAbort.thy Wed Dec 23 21:32:24 2020 +0100 +++ b/src/HOL/Hoare/HeapSyntaxAbort.thy Wed Dec 23 22:25:22 2020 +0100 @@ -3,7 +3,11 @@ Copyright 2002 TUM *) -theory HeapSyntaxAbort imports Hoare_Logic_Abort Heap begin +section \Heap syntax (abort)\ + +theory HeapSyntaxAbort + imports Hoare_Logic_Abort Heap +begin subsection "Field access and update"