| changeset 16417 | 9bc16273c2d4 |
| parent 14074 | 93dfce3b6f86 |
| child 17781 | 32bb237158a5 |
--- a/src/HOL/Hoare/Separation.thy Fri Jun 17 11:35:35 2005 +0200 +++ b/src/HOL/Hoare/Separation.thy Fri Jun 17 16:12:49 2005 +0200 @@ -13,7 +13,7 @@ *) -theory Separation = HoareAbort + SepLogHeap: +theory Separation imports HoareAbort SepLogHeap begin text{* The semantic definition of a few connectives: *}