--- a/src/HOL/UNITY/Alloc.thy Wed Jun 23 10:38:09 1999 +0200
+++ b/src/HOL/UNITY/Alloc.thy Wed Jun 23 10:38:49 1999 +0200
@@ -15,7 +15,7 @@
ALL F G. F : X --> drop_prog i F = drop_prog i G --> G : X"
- (UNITY.thy????????????????*)
+ (*UNITY.thy????????????????*)
(*An Idle program can do nothing*)
Idle :: 'a program set
"Idle == {F. Union (Acts F) <= Id}"
@@ -174,6 +174,8 @@
allocAsk = allocAsk s,
allocRel = allocRel s,
client = y |)"
+(*** "sysOfAlloc == %(s,y). s(|client := y|)" TYPE DOESN'T CHANGE***)
+
sysOfClient :: "((nat => clientState) * allocState ) => systemState"
"sysOfClient == %(x,y). sysOfAlloc(y,x)"
@@ -195,7 +197,7 @@
System_def
"System == (extend sysOfAlloc Alloc)
Join
- (extend sysOfClient (PPI x: lessThan Nclients. Client))
+ (extend sysOfClient (plam x: lessThan Nclients. Client))
Join
Network"
end