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