is mentioned by

Def ma-single-sends1(A; B; T; x; a; l; tg; f) Def == ma-single-sends(x : A; Def == ma-single-sends(a : B  rcv(l; tg) : T; Def == ma-single-sends(a; Def == ma-single-sends(l; Def == ma-single-sends([<tg,s,v. f(s(x),v)>])	[ma-single-sends1]
Def M1 || M2 Def == M1 ||decl M2 Def == & 1of(2of(2of(M1))) || 1of(2of(2of(M2))) Def == & 1of(2of(2of(2of(M1)))) || 1of(2of(2of(2of(M2)))) Def == & 1of(2of(2of(2of(2of(M1))))) || 1of(2of(2of(2of(2of(M2))))) Def == & 1of(2of(2of(2of(2of(2of(M1)))))) || 1of(2of(2of(2of(2of(2of(M2)))))) Def == & 1of(2of(2of(2of(2of(2of(2of(M1))))))) || 1of(2of(2of(2of(2of(2of(2of( Def == & 1of(2of(2of(2of(2of(2of(2of(M1))))))) || 1of(M2))))))) Def == & 1of(2of(2of(2of(2of(2of(2of(2of( Def == & 1of(M1)))))))) || 1of(2of(2of(2of(2of(2of(2of(2of(M2))))))))	[ma-compatible]
Def M1  M2 Def == 1of(M1)  1of(M2) & 1of(2of(M1))  1of(2of(M2)) Def == & 1of(2of(2of(M1)))  1of(2of(2of(M2))) Def == & & 1of(2of(2of(2of(M1))))  1of(2of(2of(2of(M2)))) Def == & & 1of(2of(2of(2of(2of(M1)))))  1of(2of(2of(2of(2of(M2))))) Def == & & 1of(2of(2of(2of(2of(2of(M1))))))  1of(2of(2of(2of(2of(2of(M2)))))) Def == & & 1of(2of(2of(2of(2of(2of(2of(M1)))))))  1of(2of(2of(2of(2of(2of(2of( Def == & & 1of(2of(2of(2of(2of(2of(2of(M1)))))))  1of(M2))))))) Def == & & 1of(2of(2of(2of(2of(2of(2of(2of( Def == & & 1of(M1))))))))  1of(2of(2of(2of(2of(2of(2of(2of(M2))))))))	[ma-sub]
Def M.send(k;l;s;v;ms;i) Def == L != 1of(2of(2of(2of(2of(2of(M))))))(<k,l>) ==> ms Def == L != 1of(2of(2of(2of(2of(2of(M))))))(<k,l>) ==> = Def == L != 1of(2of(2of(2of(2of(2of(M))))))(<k,l>) ==> if source(l) = i Def == L != 1of(2of(2of(2of(2of(2of(M))))))(<k,l>) ==> if concat(map(tgf. Def == L != 1of(2of(2of(2of(2of(2of(M))))))(<k,l>) ==> if map(x. Def == L != 1of(2of(2of(2of(2of(2of(M))))))(<k,l>) ==> if <1of(tgf),x>;2of(tgf) Def == L != 1of(2of(2of(2of(2of(2of(M))))))(<k,l>) ==> if <1of(tgf),x>;(s Def == L != 1of(2of(2of(2of(2of(2of(M))))))(<k,l>) ==> if <1of(tgf),x>;,v));L)) Def == L != 1of(2of(2of(2of(2of(2of(M))))))(<k,l>) ==> else nil fi Def == L != 1of(2of(2of(2of(2of(2of(M))))))(<k,l>) ==>  (tg:Id Def == L != 1of(2of(2of(2of(2of(2of(M))))))(<k,l>) ==>  (if source(l) = i Def == L != 1of(2of(2of(2of(2of(2of(M))))))(<k,l>) ==>  (if M.da(rcv(l; tg)) Def == L != 1of(2of(2of(2of(2of(2of(M))))))(<k,l>) ==>  (else Top fi) List	[ma-send]
Def M.dout(l,tg) == 1of(2of(M))(rcv(l; tg))?Void	[ma-dout]
Def M.din(l,tg) == 1of(2of(M))(rcv(l; tg))?Top	[ma-din]
Def MsgA Def == ds:x:Id fp-> Type Def == da:a:Knd fp-> Type Def == x:Id fp-> ds(x)?Voida:Id fp-> State(ds)ma-valtype(da; locl(a))Prop Def == kx:KndId fp-> State(ds)ma-valtype(da; 1of(kx))ds(2of(kx))?Void Def == kl:KndIdLnk fp-> (tg:Id Def == kl:KndIdLnk fp-> (State(ds)ma-valtype(da; 1of(kl)) Def == kl:KndIdLnk fp-> ((da(rcv(2of(kl); tg))?Void List)) List Def == x:Id fp-> Knd Listltg:IdLnkId fp-> Knd ListTop	[msga]

In prior sections: mb event system 1 mb event system 2 mb event system 3

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