| changeset 44871 | fbfdc5ac86be |
| parent 36866 | 426d5781bb25 |
| child 46912 | e0cd5c4df8e6 |
--- a/src/HOL/UNITY/Comp/AllocImpl.thy Sat Sep 10 21:47:55 2011 +0200 +++ b/src/HOL/UNITY/Comp/AllocImpl.thy Sat Sep 10 22:11:55 2011 +0200 @@ -5,7 +5,7 @@ header{*Implementation of a multiple-client allocator from a single-client allocator*} -theory AllocImpl imports AllocBase Follows PPROD begin +theory AllocImpl imports AllocBase "../Follows" "../PPROD" begin (** State definitions. OUTPUT variables are locals **)