equal
deleted
inserted
replaced
1 (* Title: HOL/UNITY/Comp/AllocImpl.thy |
1 (* Title: HOL/UNITY/Comp/AllocImpl.thy |
2 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
2 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
3 Copyright 1998 University of Cambridge |
3 Copyright 1998 University of Cambridge |
4 *) |
4 *) |
5 |
5 |
6 header{*Implementation of a multiple-client allocator from a single-client allocator*} |
6 section{*Implementation of a multiple-client allocator from a single-client allocator*} |
7 |
7 |
8 theory AllocImpl imports AllocBase "../Follows" "../PPROD" begin |
8 theory AllocImpl imports AllocBase "../Follows" "../PPROD" begin |
9 |
9 |
10 |
10 |
11 (** State definitions. OUTPUT variables are locals **) |
11 (** State definitions. OUTPUT variables are locals **) |