Def a declared in M == locl(a)  dom(1of(2of(M)))

is mentioned by

Thm* A:Dsys, i,a:Id. Dec(a declared in M(i))

[decidable__ma-decla]

In prior sections: mb event system 5

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