| changeset 16417 | 9bc16273c2d4 |
| parent 15074 | 277b3a4da341 |
| child 32960 | 69916a850301 |
--- a/src/HOL/UNITY/Comp/AllocImpl.thy Fri Jun 17 11:35:35 2005 +0200 +++ b/src/HOL/UNITY/Comp/AllocImpl.thy Fri Jun 17 16:12:49 2005 +0200 @@ -6,7 +6,7 @@ header{*Implementation of a multiple-client allocator from a single-client allocator*} -theory AllocImpl = AllocBase + Follows + PPROD: +theory AllocImpl imports AllocBase Follows PPROD begin (** State definitions. OUTPUT variables are locals **)