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 not otherwise mentioned in this or prior sections.

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