Def Dec(P) == P  P

is mentioned by

Thm* the_es:ES, e',e:E. Dec((e <loc e'))	[decidable__es-locl]
Thm* the_es:ES, e,e':E. Dec(e = e')	[decidable__es-E_equal]
Thm* x:A. (x,y:A. Dec(x = y))  (L:A List. Dec((x  L)))	[decidable__l_member]
Thm* a,b:IdLnk. Dec(a = b)	[decidable__equal_IdLnk]
Thm* a,b:Id. Dec(a = b)	[decidable__equal_Id]

In prior sections: core int 1 bool 1 int 2 rel 1 mb basic mb nat mb list 1 num thy 1 mb list 2 mb event system 1

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