| changeset 72990 | db8f94656024 |
| parent 69597 | ff784d5a5bfb |
| child 80914 | d97fdabd9e2b |
--- 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 \<open>Heap syntax (abort)\<close> + +theory HeapSyntaxAbort + imports Hoare_Logic_Abort Heap +begin subsection "Field access and update"