Def  == <nil,x.>

is mentioned by

Thm* ltg:(IdLnkIdType), i:Id. (ltg  da-outlinks(;i))  False	[da-outlinks-empty]
Thm* eq:EqDecider(A), B:Top, f:a:A fp-> Top.  || f	[fpf-empty-compatible-left]
Thm* eq:EqDecider(A), B:Top, f:a:A fp-> Top. f ||	[fpf-empty-compatible-right]
Def (with ds: ds Def (init: init Def action a:T Def aprecondition a(v) is Def aP) Def == mk-ma(ds; locl(a) : T; init; a : P; ; ; ; )	[ma-single-pre-init]
Def (with ds: ds Def (action a:T Def (precondition a(v) is Def (P s v) Def == mk-ma(ds; locl(a) : T; ; a : P; ; ; ; )	[ma-single-pre]
Def ma-single-sends(ds; da; k; l; f) == mk-ma(ds; da; ; ; ; <k,l> : f; ; )	[ma-single-sends]
Def ma-single-effect(ds; da; k; x; f) == mk-ma(ds; da; ; ; <k,x> : f; ; ; )	[ma-single-effect]
Def only L sends on (l with tg) == mk-ma(; ; ; ; ; ; ; <l,tg> : L)	[ma-single-sframe]
Def only members of L affect x :t == mk-ma(x : t; ; ; ; ; ; x : L; )	[ma-single-frame]
Def x : t initially x = v == mk-ma(x : t; ; x : v; ; ; ; ; )	[ma-single-init]
Def  == mk-ma(; ; ; ; ; ; ; )	[ma-empty]

In prior sections: mb event system 3

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