Def Dec(P) == P  P

is mentioned by

Thm* A:Dsys, i,a:Id. Dec(a declared in M(i))	[decidable__ma-decla]
Thm* a:Id, T,A:Type, x:Id, P:(ATProp). Thm* T Thm*  Thm* A Thm*  Thm* (a:A. Dec(v:T. P(a,v)))  Feasible(ma-single-pre1(x;A;a;T;x,v.P(x,v)))	[ma-single-pre1-feasible]
Thm* a:Id, T:Type, ds:x:Id fp-> Type, P:(State(ds)TProp). Thm* T Thm*  Thm* xdom(ds). A=ds(x)   A Thm*  Thm* (s:State(ds). Dec(v:T. P(s,v))) Thm*  Thm* Feasible((with ds: ds Thm* Faction a:T Thm* Fprecondition a(v) is Thm* FP s v))	[ma-single-pre-feasible]
Thm* x:Id, c:T, a:Id, P:(TT'Prop). Thm* T' Thm*  Thm* (u:T. Dec(v:T'. P(u,v))) Thm*  Thm* Feasible(ma-single-pre-init1(x;T;c;a;T';x,v.P(x,v)))	[ma-single-pre-init1-feasible]
Thm* P:(UnitProp). Dec(P())  Dec(x:Unit. P(x))	[decidable__ex_unit]
Thm* P:(TProp). (x:T. Dec(P(x)))  finite-type(T)  Dec(x:T. P(x))	[decidable-exists-finite]

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

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