Def once(loc;a;i)
Def == if loc = i
Def == if [ma-single-pre-init1("done";;false;a;Unit;x,v.x); 
Def == if [only members of [locl(a)] affect "done" :; 
Def == if [ma-single-effect0("done";;locl(a);Unit;x,v. true)]
Def == else nil fi

is mentioned by

Thm* a,i:Id. Thm* loc.(once(loc;a;i))  Thm* realizes es.e@i.kind(e) = locl(a) Thm* realizes es.& e@i.e'@i.kind(e) = locl(a) Thm* realizes es.& e@i.e'@i. Thm* realizes es.& kind(e') = locl(a)  Knd  e = e'  E	[once__realizes]
Thm* a,i:Id. d-feasible(loc.(once(loc;a;i)))	[once__feasible]
Thm* loc,a,i:Id. (A,Bonce(loc;a;i).A ||+ B)	[once__compatible]
Def send-once(loc;T;A;a;f;tg;l;x) Def == [(once(loc;a;source(l)));  Def == [if loc = source(l) Def == [if ma-single-sends1(A; Unit; T; x; locl(a); l; tg; (a,b. [(f(a))])) Def == [else  fi]	[send-once]

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