Who Cites ma-single-pre-init?
ma-single-pre-init	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; ; ; ; )
fpf-empty	Def  == <nil,x.>
fpf-single	Def x : v == <[x],x.v>
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:

(with ds: ds (init: init action a:T aprecondition a(v) is aP)

has structure:

ma-single-pre-init(ds; init; a; T; P)

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