equal
deleted
inserted
replaced
1 (* Title: ZF/UNITY/AllocBase.thy |
1 (* Title: ZF/UNITY/AllocBase.thy |
2 Author: Sidi O Ehmety, Cambridge University Computer Laboratory |
2 Author: Sidi O Ehmety, Cambridge University Computer Laboratory |
3 Copyright 2001 University of Cambridge |
3 Copyright 2001 University of Cambridge |
4 *) |
4 *) |
5 |
5 |
6 header{*Common declarations for Chandy and Charpentier's Allocator*} |
6 section{*Common declarations for Chandy and Charpentier's Allocator*} |
7 |
7 |
8 theory AllocBase imports Follows MultisetSum Guar begin |
8 theory AllocBase imports Follows MultisetSum Guar begin |
9 |
9 |
10 abbreviation (input) |
10 abbreviation (input) |
11 tokbag :: i (* tokbags could be multisets...or any ordered type?*) |
11 tokbag :: i (* tokbags could be multisets...or any ordered type?*) |