# HG changeset patch
# User paulson
# Date 930127129 -7200
# Node ID 5a557122bb62eb46b9dd333d6c12a4979bf4ede0
# Parent  0e5c82abfc71dbd7b6640543f032d88004670f7e
renamed PPI to plam

diff -r 0e5c82abfc71 -r 5a557122bb62 src/HOL/UNITY/Alloc.thy
--- 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