Def		MsgA	[msga]
Def		a declared in M	[ma-decla]
Def		ma-outlinks(M;i)	[ma-outlinks]
Def		M.din(l,tg)	[ma-din]
Def		M.dout(l,tg)	[ma-dout]
Def		M.init(x,v)	[ma-init]
Def		M.state	[ma-st]
Def		M.V(k)	[ma-v]
Def		unsolvable M.pre(a,s)	[ma-npre]
Def		M.pre(a,s,v)	[ma-pre]
Def		M.ef(k,x,s,v,w)	[ma-ef]
Def		tagged-messages(l;s;v;L)	[tagged-messages]
Def		M.send(k;l;s;v;ms;i)	[ma-send]
Def		M sends on link l	[ma-sends-on]
Def		M1  M2	[ma-sub]
Def		ma-is-empty(M)	[ma-is-empty]
Def		ma-single-effect0(x;A;k;T;f)	[ma-single-effect0]
Def		ma-single-effect1(x;A;y;B;k;T;f)	[ma-single-effect1]
Def		ma-single-sends1(A; B; T; x; a; l; tg; f)	[ma-single-sends1]
Def		ma-single-pre1(x;A;a;T;y,v.P(y;v))	[ma-single-pre1]
Def		ma-single-pre-init1(x;T;c;a;T';y,v.P(y;v))	[ma-single-pre-init1]
Def		A ||+ B	[ma-compat]
Def		(L)	[ma-join-list]
Def		MsgAForm	[msg-form]
Def		P  Q	[or]	core
Def		EqDecider(T)	[deq]	mb event system 2
Def		P  Q	[iff]	core
Def		Feasible(M)	[ma-feasible]
Def		M1 || M2	[ma-compatible]
Def		ma-valtype(da; k)	[ma-valtype]
Def		State(ds)	[ma-state]
Def		M.da(a)	[ma-da]
Def		M.ds(x)	[ma-ds]
Def		M1  M2	[ma-join]
Def		f  g	[fpf-join]
Def		f(x)?z	[fpf-cap]	mb event system 3
Def		M.sframe(k sends <l,tg>)	[ma-sframe]
Def		M.frame(k affects x)	[ma-frame]
Def		z != f(x) ==> P(a;z)	[fpf-val]	mb event system 3
Def		f  g	[fpf-sub]	mb event system 3
Def		M1 ||decl M2	[ma-compatible-decls]
Def		f || g	[fpf-compatible]
Def		xdom(f). v=f(x)   P(x;v)	[fpf-all]
Def		ma-sframe-compatible(A; B)	[ma-sframe-compatible]
Def		ma-frame-compatible(A; B)	[ma-frame-compatible]
Def		x  dom(f)	[fpf-dom]	mb event system 3
Def		da-outlinks(da;i)	[da-outlinks]
Def		has-src(i;k)	[has-src]	mb event system 2
Def		a = b	[eq_id]	mb event system 2
Def		deq-member(eq;x;L)	[deq-member]	mb event system 2
Def		eqof(d)	[eqof]	mb event system 2
Def		True	[true]	core
Def		False	[false]	core
Def		x : t initially x = v	[ma-single-init]
Def		only members of L affect x :t	[ma-single-frame]
Def		only L sends on (l with tg)	[ma-single-sframe]
Def		da-outlink-f(da;k)	[da-outlink-f]
Def		f(x)	[fpf-ap]	mb event system 3
Def		KindDeq	[Kind-deq]	mb event system 2
Def		IdLnkDeq	[idlnk-deq]	mb event system 2
Def		IdDeq	[id-deq]	mb event system 2
Def		product-deq(A;B;a;b)	[product-deq]	mb event system 2
Def		prod-deq(A;B;a;b)	[prod-deq]	mb event system 2
Def		b	[assert]	bool 1
Def		P & Q	[and]	core
Def		P  Q	[implies]	core
Def		x:A. B(x)	[all]	core
Def		a:A fp-> B(a)	[fpf]	mb event system 3
Def		(x  l)	[l_member]	mb list 1
Def		l[i]	[select]	list 1
Def		nth_tl(n;as)	[nth_tl]	list 1
Def		ij	[le_int]	bool 1
Def		b	[bnot]	bool 1
Def		mapfilter(f;P;L)	[mapfilter]	mb list 2
Def		filter(P;l)	[filter]	mb list 1
Def		lnk(k)	[lnk]	mb event system 2
Def		fpf-dom-list(f)	[fpf-dom-list]
Def		tagged-list-messages(s;v;L)	[tagged-list-messages]
Def		source(l)	[lsrc]	mb event system 2
Def		fpf-is-empty(f)	[fpf-is-empty]	mb event system 3
Def		union-deq(A;B;a;b)	[union-deq]	mb event system 2
Def		proddeq(a;b)	[proddeq]	mb event system 2
Def		sumdeq(a;b)	[sumdeq]	mb event system 2
Def		1of(t)	[pi1]	core
Def		concat(ll)	[concat]	mb event system 1
Def		as @ bs	[append]	list 1
Def		Top	[top]	core
Def		Knd	[Knd]	mb event system 1
Def		IdLnk	[IdLnk]	mb event system 1
Def		Id	[Id]	mb event system 1
Def		rcv(l; tg)	[rcv]	mb event system 1
Def		tag(k)	[tagof]	mb event system 2
Def		2of(t)	[pi2]	core
Def		Prop	[prop]	core
Def		(with ds: ds (action a:T (precondition a(v) is (P s v)	[ma-single-pre]
Def		(with ds: ds (init: init action a:T aprecondition a(v) is aP)	[ma-single-pre-init]
Def		locl(a)	[locl]	mb event system 1
Def		Dec(P)	[decidable]	core
Def			[nat]	int 1
Def		AB	[le]	core
Def		A	[not]	core
Def		map(f;as)	[map]	list 1
Def		if b t else f fi	[ifthenelse]	bool 1
Def		A & B	[cand]	core
Def			[it]	core
Def		ma-single-effect(ds; da; k; x; f)	[ma-single-effect]
Def		ma-single-sends(ds; da; k; l; f)	[ma-single-sends]
Def			[ma-empty]
Def			[fpf-empty]	mb event system 3
Def		mk-ma(ds; da; init; pre; ef; send; frame; sframe)	[mk-ma]
Def		pq	[band]	bool 1
Def		x : v	[fpf-single]
Def		x:A. B(x)	[exists]	core
Def		reduce(f;k;as)	[reduce]	list 1
Def		1,2. b(1;2)	[so_lambda2]
Def		P  Q	[rev_implies]	core
Def		NatDeq	[nat-deq]	mb event system 2
Def		AtomDeq	[atom-deq]	mb event system 2
Def		outl(x)	[outl]	union
Def		isrcv(k)	[isrcv]	mb event system 1
Def		p  q	[bor]	bool 1
Def		||as||	[length]	list 1
Def		i=j	[eq_int]	bool 1
Def		x=yAtom	[eq_atom]	bool 1
Def		sum-deq(A;B;a;b)	[sum-deq]	mb event system 2
Def		isl(x)	[isl]	union
Def		hd(l)	[hd]	list 1
Def		tl(l)	[tl]	list 1
Def		i<j	[lt_int]	bool 1

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