# HG changeset patch
# User paulson
# Date 959078118 -7200
# Node ID ac2aac644b9fb8d796e720ef49607bce31a3e29b
# Parent  cb419b8498e5477251d596d1f0b2126772b52058
use of AllocBase

diff -r cb419b8498e5 -r ac2aac644b9f 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