Who Cites ma-single-pre1?
ma-single-pre1	Def ma-single-pre1(x;A;a;T;y,v.P(y;v)) Def == (with ds: x : A Def == (action a:T Def == (precondition a(v) is Def == (s,v. P(s(x);v) s v)
so_lambda2	Def (1,2. b(1;2))(1,2) == b(1;2)
ma-single-pre	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; ; ; ; )
fpf-single	Def x : v == <[x],x.v>
fpf-empty	Def  == <nil,x.>
locl	Def locl(a) == inr(a)
	Thm* a:Id. locl(a)  Knd
mk-ma	Def mk-ma(ds; da; init; pre; ef; send; frame; sframe) Def == <ds,da,init,pre,ef,send,frame,sframe,>

Syntax:

ma-single-pre1(x;A;a;T;y,v.P(y;v))

has structure:

ma-single-pre1(x; A; a; T; y,v.P(y;v))

About: IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html