Def f(x)?z == if x  dom(f) f(x) else z fi

is mentioned by

Thm* a:Id, T:Top, ds:x:Id fp-> Type, P:Top, init:x:Id fp-> ds(x)?Void, x:Id, Thm* t:Type, v:t. Thm* ds || x : t Thm*  Thm* (x  dom(init)  init(x) = v  t) Thm*  Thm* (with ds: ds Thm* (init: init Thm* action a:T Thm* aprecondition a(v) is Thm* aP) ||+ x : t initially x = v

[ma-single-pre-init-ma-single-init-compatible]

In prior sections: mb event system 4 mb event system 5 mb event system 6

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