# HG changeset patch
# User paulson
# Date 928830604 -7200
# Node ID 9ee166138311597fbc80e85c08c148a59f68b76f
# Parent  95abcc002a21992779be6e05fe877adc6bd60271
removed obsolete "Prefix" ancestor

diff -r 95abcc002a21 -r 9ee166138311 src/HOL/UNITY/Client.thy
--- a/src/HOL/UNITY/Client.thy	Tue Jun 08 10:25:12 1999 +0200
+++ b/src/HOL/UNITY/Client.thy	Tue Jun 08 10:30:04 1999 +0200
@@ -6,7 +6,7 @@
 Distributed Resource Management System: the Client
 *)
 
-Client = Comp + Prefix + 
+Client = Comp + 
 
 consts
   Max :: nat       (*Maximum number of tokens*)