src/HOL/UNITY/AllocBase.thy

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/UNITY/AllocBase.thy	Tue May 23 12:31:38 2000 +0200
@@ -0,0 +1,24 @@
+(*  Title:      HOL/UNITY/AllocBase
+    ID:         $Id$
+    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   1998  University of Cambridge
+
+Common declarations for Chandy and Charpentier's Allocator
+*)
+
+AllocBase = Rename + Follows + 
+
+consts
+  NbT      :: nat       (*Number of tokens in system*)
+  Nclients :: nat       (*Number of clients*)
+
+rules
+  NbT_pos  "0 < NbT"
+
+(*This function merely sums the elements of a list*)
+consts tokens     :: nat list => nat
+primrec 
+  "tokens [] = 0"
+  "tokens (x#xs) = x + tokens xs"
+
+end