author | paulson |
Tue, 23 May 2000 12:35:18 +0200 | |
changeset 8931 | ac2aac644b9f |
parent 8930 | cb419b8498e5 |
child 8932 | c1d0f7495714 |
--- a/src/HOL/UNITY/Client.thy Tue May 23 12:34:26 2000 +0200 +++ b/src/HOL/UNITY/Client.thy Tue May 23 12:35:18 2000 +0200 @@ -6,10 +6,7 @@ Distributed Resource Management System: the Client *) -Client = Rename + - -consts - NbT :: nat (*Maximum number of tokens*) +Client = Rename + AllocBase + types tokbag = nat (*tokbags could be multisets...or any ordered type?*) @@ -63,7 +60,4 @@ client_map :: "'a state_u => state*'a" "client_map == funPair non_extra extra" -rules - NbT_pos "0 < NbT" - end