Def mk-ma(ds; da; init; pre; ef; send; frame; sframe)
Def == <ds,da,init,pre,ef,send,frame,sframe,>

is mentioned by

Def (with ds: ds Def (init: init Def action a:T Def aprecondition a(v) is Def aP) Def == mk-ma(ds; locl(a) : T; init; a : P; ; ; ; )	[ma-single-pre-init]
Def (with ds: ds Def (action a:T Def (precondition a(v) is Def (P s v) Def == mk-ma(ds; locl(a) : T; ; a : P; ; ; ; )	[ma-single-pre]
Def ma-single-sends(ds; da; k; l; f) == mk-ma(ds; da; ; ; ; <k,l> : f; ; )	[ma-single-sends]
Def ma-single-effect(ds; da; k; x; f) == mk-ma(ds; da; ; ; <k,x> : f; ; ; )	[ma-single-effect]
Def only L sends on (l with tg) == mk-ma(; ; ; ; ; ; ; <l,tg> : L)	[ma-single-sframe]
Def only members of L affect x :t == mk-ma(x : t; ; ; ; ; ; x : L; )	[ma-single-frame]
Def x : t initially x = v == mk-ma(x : t; ; x : v; ; ; ; ; )	[ma-single-init]
Def M1  M2 Def == mk-ma(1of(M1)  1of(M2); Def == mk-ma(1of(2of(M1))  1of(2of(M2)); Def == mk-ma(1of(2of(2of(M1)))  1of(2of(2of(M2))); Def == mk-ma(1of(2of(2of(2of(M1))))  1of(2of(2of(2of(M2)))); Def == mk-ma(1of(2of(2of(2of(2of(M1)))))  1of(2of(2of(2of(2of(M2))))); Def == mk-ma(1of(2of(2of(2of(2of(2of(M1))))))  1of(2of(2of(2of(2of(2of( Def == mk-ma(1of(2of(2of(2of(2of(2of(M1))))))  1of(M2)))))); Def == mk-ma(1of(2of(2of(2of(2of(2of(2of( Def == mk-ma(1of(M1)))))))  1of(2of(2of(2of(2of(2of(2of(M2))))))); Def == mk-ma(1of(2of(2of(2of(2of(2of(2of(2of( Def == mk-ma(1of(M1))))))))  1of(2of(2of(2of(2of(2of(2of(2of(M2)))))))))	[ma-join]
Def  == mk-ma(; ; ; ; ; ; ; )	[ma-empty]

Try larger context: EventSystems IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html