Def ma-single-pre1(x;A;a;T;y,v.P(y;v))
Def == (with ds: x : A
Def == (action a:T
Def == (precondition a(v) is
Def == (s,v. P(s(x);v) s v)

is mentioned by

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]

In prior sections: mb event system 6

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