renamed PPI to plam
authorpaulson
Wed, 23 Jun 1999 10:38:49 +0200 (1999-06-23)
changeset 6841 5a557122bb62
parent 6840 0e5c82abfc71
child 6842 56e08e264961
renamed PPI to plam
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