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

In prior sections: mb event system 6 mb event system 7

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html