Def		sends(l,tg,e)	[es-tg-sends]
Def		e@i.P(e)	[existse-at]
Def		withlnk(l;mss)	[w-withlnk]
Def		w-tagged(tg; mss)	[w-tagged]
Def		(x initially i)	[w-initially]
Def		f(x)?z	[fpf-cap]
Def		z != f(x) ==> P(a;z)	[fpf-val]
Def			[bool]	bool 1
Def		ES	[event_system]	mb event system 2
Def		e  e'	[es-le]	mb event system 2
Def		ESAxioms{i:l} ESAxioms(E; ESAxioms(T; ESAxioms(M; ESAxioms(loc; ESAxioms(kind; ESAxioms(val; ESAxioms(when; ESAxioms(after; ESAxioms(sends; ESAxioms(sender; ESAxioms(index; ESAxioms(first; ESAxioms(pred; ESAxioms(causl)	[ESAxioms]	mb event system 2
Def		EqDecider(T)	[deq]	mb event system 2
Def		P  Q	[iff]	core
Def		(Msg on l)	[es-Msgl]	mb event system 2
Def		Msg	[es-Msg]	mb event system 2
Def		(e <loc e')	[es-locl]	mb event system 2
Def		[e, e']	[es-interval]
Def		(x after e)	[es-after]	mb event system 2
Def		vartype(i;x)	[es-vartype]	mb event system 2
Def		Prop	[prop]	core
Def		@i always.P(v)	[alle-at1]
Def		Dec(P)	[decidable]	core
Def		rcv(l; tg)	[rcv]	mb event system 1
Def		valtype(e)	[es-valtype]	mb event system 2
Def		rcvtype(e)	[es-rcvtype]	mb event system 2
Def		tag(e)	[es-tag]	mb event system 2
Def		lnk(e)	[es-lnk]	mb event system 2
Def		isrcv(e)	[es-isrcv]	mb event system 2
Def		acttype(e)	[es-acttype]	mb event system 2
Def		act(e)	[es-act]	mb event system 2
Def		kind(e)	[es-kind]	mb event system 2
Def		sender(e)	[es-sender]	mb event system 2
Def		{T}	[guard]	core
Def		World	[world]
Def		Action(i)	[w-action]
Def		valtype(i;a)	[w-valtype]
Def		FairFifo	[fair-fifo]
Def		p = q	[w-eq-E]
Def		Msg_sub(l; M)	[Msg_sub]	mb event system 1
Def		{i..j}	[int_seg]	int 1
Def		a:A fp-> B(a)	[fpf]
Def		(x  l)	[l_member]	mb list 1
Def		l[i]	[select]	list 1
Def		ES(the_w)	[w-es]
Def		strong-subtype(A;B)	[strong-subtype]	mb event system 1
Def			[fpf-empty]
Def		fpf-is-empty(f)	[fpf-is-empty]
Def		f  g	[fpf-sub]
Def		false	[bfalse]	bool 1
Def		true	[btrue]	bool 1
Def		mtag(m)	[es-mtag]
Def		mtag(m)	[mtag]	mb event system 1
Def		before(e)	[es-before]
Def		pred(e)	[es-pred]	mb event system 2
Def		queue(l;t)	[w-queue]
Def		e <c e'	[w-causl]
Def		index(e)	[w-index]
Def		sender(e)	[w-sender]
Def		match(l;t;t')	[w-match]
Def		snds(l;t)	[w-snds]
Def		rcvs(l;t)	[w-rcvs]
Def		upto(n)	[upto]	mb event system 1
Def		concat(ll)	[concat]	mb event system 1
Def		as @ bs	[append]	list 1
Def		first(e)	[es-first]	mb event system 2
Def		if b t else f fi	[ifthenelse]	bool 1
Def		Y	[ycomb]	core
Def		es-ble{i:l}(es;e;e')	[es-ble]
Def		mapfilter(f;P;L)	[mapfilter]	mb list 2
Def		m(l;t)	[w-ml]
Def		sends(l;e)	[w-sends]
Def		onlnk(l;mss)	[w-onlnk]
Def		filter(P;l)	[filter]	mb list 1
Def		sends(l;e)	[es-sends]	mb event system 2
Def		w-action-dec(TA;M;i)	[w-action-dec]
Def		a = b	[eq_id]	mb event system 2
Def		e@i.P(e)	[alle-at]
Def		loc(e)	[es-loc]	mb event system 2
Def		action(dec)	[action]
Def		Knd	[Knd]	mb event system 1
Def		Msg	[w-Msg]
Def		Msg(M)	[Msg]	mb event system 1
Def		haslink(l; m)	[haslink]	mb event system 1
Def		IdLnk	[IdLnk]	mb event system 1
Def		isrcv(l;a)	[w-isrcvl]
Def		a = b	[eq_lnk]	mb event system 2
Def		e <loc e'	[w-locl]
Def		E	[w-E]
Def		IdLnkDeq	[idlnk-deq]	mb event system 2
Def		Id	[Id]	mb event system 1
Def		P  Q	[implies]	core
Def		E	[es-E]	mb event system 2
Def		x:A. B(x)	[all]	core
Def		(x when e)	[es-when]	mb event system 2
Def		P & Q	[and]	core
Def		x:A. B(x)	[exists]	core
Def		Unit	[unit]	core
Def		destination(l)	[ldst]	mb event system 2
Def		V(i;k)	[w-V]
Def		eventtype(k;loc;V;M;e)	[eventtype]	mb event system 2
Def		kindcase(k;a.f(a);l,t.g(l;t))	[kindcase]	mb event system 2
Def		Top	[top]	core
Def		mlnk(m)	[mlnk]	mb event system 1
Def		source(l)	[lsrc]	mb event system 2
Def		IdDeq	[id-deq]	mb event system 2
Def		SWellFounded(R(x;y))	[strongwellfounded]	mb event system 2
Def			[nat]	int 1
Def		vartype(i;x)	[w-vartype]
Def		w.T	[w-T]
Def		w.M	[w-M]
Def		w.TA	[w-TA]
Def		msg(a)	[w-msg]
Def		kind(e)	[w-ekind]
Def		kind(a)	[w-kind]
Def		lnk(k)	[lnk]	mb event system 2
Def		m(i;t)	[w-m]
Def		val(e)	[w-eval]
Def		act(e)	[w-act]
Def		pred(e)	[w-pred]
Def		first(e)	[w-first]
Def		a(i;t)	[w-a]
Def		(x after e)	[w-after]
Def		(x when e)	[w-when]
Def		s(i;t).x	[w-s]
Def		loc(e)	[w-loc]
Def		product-deq(A;B;a;b)	[product-deq]	mb event system 2
Def		x  dom(f)	[fpf-dom]
Def		deq-member(eq;x;L)	[deq-member]	mb event system 2
Def		(e < e')	[es-causl]	mb event system 2
Def		eqof(d)	[eqof]	mb event system 2
Def		proddeq(a;b)	[proddeq]	mb event system 2
Def		1of(t)	[pi1]	core
Def		val(a)	[w-val]
Def		tag(k)	[tagof]	mb event system 2
Def		time(e)	[w-time]
Def		f(x)	[fpf-ap]
Def		2of(t)	[pi2]	core
Def		isrcv(k)	[isrcv]	mb event system 1
Def		isnull(a)	[w-isnull]
Def		islocal(k)	[islocal]	mb event system 1
Def		isl(x)	[isl]	union
Def		act(k)	[actof]	mb event system 2
Def		outr(x)	[outr]	union
Def		nth_tl(n;as)	[nth_tl]	list 1
Def		ij	[le_int]	bool 1
Def		b	[bnot]	bool 1
Def		prod-deq(A;B;a;b)	[prod-deq]	mb event system 2
Def		pq	[band]	bool 1
Def		map(f;as)	[map]	list 1
Def		||as||	[length]	list 1
Def		P  Q	[or]	core
Def		ij	[ge]	core
Def		i  j < k	[lelt]	int 1
Def		AB	[le]	core
Def		hd(l)	[hd]	list 1
Def		A & B	[cand]	core
Def		b	[assert]	bool 1
Def		A	[not]	core
Def		R^+	[rel_plus]	mb event system 2
Def		NatDeq	[nat-deq]	mb event system 2
Def		R^n	[rel_exp]	mb nat
Def		i=j	[eq_int]	bool 1
Def		i<j	[lt_int]	bool 1
Def		mu(f)	[mu]	mb event system 1
Def		x f y	[infix_ap]	core
Def			[it]	core
Def		locl(a)	[locl]	mb event system 1
Def		P  Q	[rev_implies]	core
Def		Trans x,y:T. E(x;y)	[trans]	rel 1
Def		reduce(f;k;as)	[reduce]	list 1
Def		outl(x)	[outl]	union
Def		tl(l)	[tl]	list 1
Def			[nat_plus]	int 1
Def		AtomDeq	[atom-deq]	mb event system 2
Def		p  q	[bor]	bool 1
Def		x=yAtom	[eq_atom]	bool 1

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