equal
deleted
inserted
replaced
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
4 Copyright 2000 University of Cambridge |
4 Copyright 2000 University of Cambridge |
5 |
5 |
6 Implementation of a multiple-client allocator from a single-client allocator |
6 Implementation of a multiple-client allocator from a single-client allocator |
7 |
|
8 add_path "../Induct"; |
|
9 time_use_thy "AllocImpl"; |
|
10 *) |
7 *) |
11 |
8 |
12 AddIs [impOfSubs subset_preserves_o]; |
9 AddIs [impOfSubs subset_preserves_o]; |
13 Addsimps [funPair_o_distrib]; |
10 Addsimps [funPair_o_distrib]; |
14 Addsimps [Always_INT_distrib]; |
11 Addsimps [Always_INT_distrib]; |