changeset 35316 | 870dfea4f9c0 |
parent 35113 | 1a0c129bb2e0 |
child 41959 | b460124855b8 |
--- a/src/HOL/Hoare/HeapSyntaxAbort.thy Tue Feb 23 10:11:12 2010 +0100 +++ b/src/HOL/Hoare/HeapSyntaxAbort.thy Tue Feb 23 10:11:15 2010 +0100 @@ -3,7 +3,7 @@ Copyright 2002 TUM *) -theory HeapSyntaxAbort imports HoareAbort Heap begin +theory HeapSyntaxAbort imports Hoare_Logic_Abort Heap begin subsection "Field access and update"