src/HOL/UNITY/Client.thy

--- 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