Def recognizer1(loc;T;A;P;k;i;r;x)
Def == if loc = i
Def == if [r :  initially r = false; 
Def == if [only members of [k] affect r :; 
Def == if [ma-single-effect1(r;;x;A;k;T;r,x,v. P(x,v)  r)]
Def == else nil fi

is mentioned by

Thm* P:(AT), k:Knd, i,r,x:Id. Thm* A Thm*  Thm* T Thm*  Thm* x = r Thm*  Thm* loc.(recognizer1(loc;T;A;P;k;i;r;x))  Thm* realizes es.e@i.kind(e) = k  Knd  (valtype(e) r T) Thm* realizes es.& (vartype(i;x) r A) Thm* realizes es.& e@i.first(e)  (r when e) = false   Thm* realizes es.& e'@i.(r after e') Thm* realizes es.& e'@i. Thm* realizes es.& e'@i.(e:E.  Thm* realizes es.& e'@i.((e <loc e')  e = e'  E Thm* realizes es.& e'@i.(& kind(e) = k  Knd Thm* realizes es.& e'@i.(& P((x when e),val(e)))	[recognizer1__realizes]
Thm* P:(AT), k:Knd, i,r,x:Id. Thm* A  T  x = r  d-feasible(loc.(recognizer1(loc;T;A;P;k;i;r;x)))	[recognizer1__feasible]
Thm* loc:Id, T,A:Type, P:(AT), k:Knd, i,r,x:Id. Thm* A  T  x = r  (A,Brecognizer1(loc;T;A;P;k;i;r;x).A ||+ B)	[recognizer1__compatible]
Def trigger1(loc;T;A;P;i;k;a;x) Def == [(recognizer1(loc;T;A;P;k;i;"trigger";x));  Def == [if loc = i ma-single-pre1("trigger";;a;Unit;x,v.x) else  fi]	[trigger1]

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