src/HOL/UNITY/Alloc.thy

   modular :: "['a, ('a=>'b) program set] => bool"
     "modular i X ==
        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}"
 
 (*simplifies the expression of some specifications*)

   sysOfAlloc :: "(allocState * (nat => clientState)) => systemState"
     "sysOfAlloc == %(s,y). (| allocGiv = allocGiv s,
 			      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)"
 
 

 
   defines
     System_def
       "System == (extend sysOfAlloc Alloc)
                  Join
-                 (extend sysOfClient (PPI x: lessThan Nclients. Client))
+                 (extend sysOfClient (plam x: lessThan Nclients. Client))
                  Join
                  Network"
 end