Def		D  realizes es.P(es)	[d-realizes]
Def		D1  D2	[d-sub]	mb event system 5
Def		M1  M2	[ma-sub]	mb event system 4
Def		@i: A	[m-sys-at]
Def		es is an event system of D	[d-es]
Def		ES	[event_system]	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		A ||+ B	[ma-compat]	mb event system 4
Def		M1 || M2	[ma-compatible]	mb event system 4
Def		d-feasible(D)	[d-feasible]	mb event system 5
Def		interface-check(D;l;tg;T)	[interface-check]	mb event system 5
Def		M.din(l,tg)	[ma-din]	mb event system 4
Def		D realizes2 es.P(es)	[d-realizes2]
Def		System	[msystem]
Def		PossibleWorld(D;w)	[possible-world]	mb event system 5
Def		Dsys	[dsys]	mb event system 5
Def		MsgA	[msga]	mb event system 4
Def		M.dout(l,tg)	[ma-dout]	mb event system 4
Def		M.send(k;l;s;v;ms;i)	[ma-send]	mb event system 4
Def		rcv(l; tg)	[rcv]	mb event system 1
Def		ma-frame-compatible(A; B)	[ma-frame-compatible]	mb event system 4
Def		ma-sframe-compatible(A; B)	[ma-sframe-compatible]	mb event system 4
Def		(L)	[ma-join-list]	mb event system 4
Def		M1  M2	[ma-join]	mb event system 4
Def		MsgAForm	[msg-form]	mb event system 4
Def		World	[world]	mb event system 3
Def		Feasible(M)	[ma-feasible]	mb event system 4
Def		M1 ||decl M2	[ma-compatible-decls]	mb event system 4
Def		M.ef(k,x,s,v,w)	[ma-ef]	mb event system 4
Def		Action(i)	[w-action]	mb event system 3
Def		action(dec)	[action]	mb event system 3
Def		Knd	[Knd]	mb event system 1
Def		ma-outlinks(M;i)	[ma-outlinks]	mb event system 4
Def		ma-valtype(da; k)	[ma-valtype]	mb event system 4
Def		a declared in M	[ma-decla]	mb event system 4
Def		da-outlinks(da;i)	[da-outlinks]	mb event system 4
Def		unsolvable M.pre(a,s)	[ma-npre]	mb event system 4
Def		M.sframe(k sends <l,tg>)	[ma-sframe]	mb event system 4
Def		M.frame(k affects x)	[ma-frame]	mb event system 4
Def		M.da(a)	[ma-da]	mb event system 4
Def		da-outlink-f(da;k)	[da-outlink-f]	mb event system 4
Def		KindDeq	[Kind-deq]	mb event system 2
Def		Msg	[es-Msg]	mb event system 2
Def		FairFifo	[fair-fifo]	mb event system 3
Def		Msg_sub(l; M)	[Msg_sub]	mb event system 1
Def		Msg	[w-Msg]	mb event system 3
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			[bool]	bool 1
Def		finite-type(T)	[finite-type]	mb event system 1
Def		Dec(P)	[decidable]	core
Def		Prop	[prop]	core
Def			[it]	core
Def		Unit	[unit]	core
Def		ma-single-pre-init1(x;T;c;a;T';y,v.P(y;v))	[ma-single-pre-init1]	mb event system 4
Def		@i (with ds: ds @i init: init @i action a:T @i precondition a(v) is @i P s v)	[d-single-pre-init]	mb event system 5
Def		(with ds: ds (init: init action a:T aprecondition a(v) is aP)	[ma-single-pre-init]	mb event system 4
Def		State(ds)	[ma-state]	mb event system 4
Def		@i: x:T @i: xinitially x = v	[d-single-init]	mb event system 5
Def		@i: only L affects x : t	[d-single-frame]	mb event system 5
Def		sends(l,tg,e)	[es-tg-sends]	mb event system 3
Def		@i: only L sends on (l with tg)	[d-single-sframe]	mb event system 5
Def		d-single-effect(i; ds; da; k; x; f)	[d-single-effect]	mb event system 5
Def		d-single-sends(i; ds; da; k; l; f)	[d-single-sends]	mb event system 5
Def		@i (with ds: ds @i action a:T @i precondition a(v) is @i P s v)	[d-single-pre]	mb event system 5
Def		ma-single-effect1(x;A;y;B;k;T;f)	[ma-single-effect1]	mb event system 4
Def		ES(the_w)	[w-es]	mb event system 3
Def		w-tagged(tg; mss)	[w-tagged]	mb event system 3
Def		w-action-dec(TA;M;i)	[w-action-dec]	mb event system 3
Def		has-src(i;k)	[has-src]	mb event system 2
Def		a = b	[eq_id]	mb event system 2
Def		M sends on link l	[ma-sends-on]	mb event system 4
Def		e <c e'	[w-causl]	mb event system 3
Def		index(e)	[w-index]	mb event system 3
Def		sender(e)	[w-sender]	mb event system 3
Def		sends(l;e)	[w-sends]	mb event system 3
Def		queue(l;t)	[w-queue]	mb event system 3
Def		match(l;t;t')	[w-match]	mb event system 3
Def		snds(l;t)	[w-snds]	mb event system 3
Def		m(l;t)	[w-ml]	mb event system 3
Def		onlnk(l;mss)	[w-onlnk]	mb event system 3
Def		withlnk(l;mss)	[w-withlnk]	mb event system 3
Def		rcvs(l;t)	[w-rcvs]	mb event system 3
Def		isrcv(l;a)	[w-isrcvl]	mb event system 3
Def		a = b	[eq_lnk]	mb event system 2
Def		IdLnkDeq	[idlnk-deq]	mb event system 2
Def		M.ds(x)	[ma-ds]	mb event system 4
Def		M.pre(a,s,v)	[ma-pre]	mb event system 4
Def		M.init(x,v)	[ma-init]	mb event system 4
Def		IdDeq	[id-deq]	mb event system 2
Def		f  g	[fpf-join]	mb event system 4
Def		f(x)?z	[fpf-cap]	mb event system 3
Def		a:A fp-> B(a)	[fpf]	mb event system 3
Def		{T}	[guard]	core
Def		(xL.P(x))	[l_all]	mb list 2
Def		(x,yL.P(x;y))	[pairwise]	mb event system 1
Def		(x  l)	[l_member]	mb list 1
Def		ma-is-empty(M)	[ma-is-empty]	mb event system 4
Def		true	[btrue]	bool 1
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		proddeq(a;b)	[proddeq]	mb event system 2
Def		pq	[band]	bool 1
Def		xdom(f). v=f(x)   P(x;v)	[fpf-all]	mb event system 4
Def		tagged-messages(l;s;v;L)	[tagged-messages]	mb event system 4
Def		tagged-list-messages(s;v;L)	[tagged-list-messages]	mb event system 4
Def		f  g	[fpf-sub]	mb event system 3
Def		f || g	[fpf-compatible]	mb event system 4
Def		z != f(x) ==> P(a;z)	[fpf-val]	mb event system 3
Def		x  dom(f)	[fpf-dom]	mb event system 3
Def		deq-member(eq;x;L)	[deq-member]	mb event system 2
Def		mapfilter(f;P;L)	[mapfilter]	mb list 2
Def		filter(P;l)	[filter]	mb list 1
Def		concat(ll)	[concat]	mb event system 1
Def		reduce(f;k;as)	[reduce]	list 1
Def		True	[true]	core
Def		E	[w-E]	mb event system 3
Def		b	[assert]	bool 1
Def		P  Q	[or]	core
Def		ma-single-effect0(x;A;k;T;f)	[ma-single-effect0]	mb event system 4
Def		ma-single-effect(ds; da; k; x; f)	[ma-single-effect]	mb event system 4
Def		ma-single-pre1(x;A;a;T;y,v.P(y;v))	[ma-single-pre1]	mb event system 4
Def		(with ds: ds (action a:T (precondition a(v) is (P s v)	[ma-single-pre]	mb event system 4
Def		ma-single-sends(ds; da; k; l; f)	[ma-single-sends]	mb event system 4
Def		M(i)	[d-m]	mb event system 5
Def		destination(l)	[ldst]	mb event system 2
Def		(x when e)	[es-when]	mb event system 2
Def		first(e)	[es-first]	mb event system 2
Def		valtype(e)	[es-valtype]	mb event system 2
Def		(e <loc e')	[es-locl]	mb event system 2
Def		acttype(e)	[es-acttype]	mb event system 2
Def		loc(e)	[es-loc]	mb event system 2
Def		vartype(i;x)	[es-vartype]	mb event system 2
Def		rcvtype(e)	[es-rcvtype]	mb event system 2
Def		lnk(e)	[es-lnk]	mb event system 2
Def		isrcv(e)	[es-isrcv]	mb event system 2
Def		tag(e)	[es-tag]	mb event system 2
Def		act(e)	[es-act]	mb event system 2
Def		kind(e)	[es-kind]	mb event system 2
Def		(x after e)	[es-after]	mb event system 2
Def		val(e)	[es-val]	mb event system 2
Def		sends(l;e)	[es-sends]	mb event system 2
Def		sender(e)	[es-sender]	mb event system 2
Def		f(x)	[fpf-ap]	mb event system 3
Def		mtag(m)	[es-mtag]	mb event system 3
Def		V(i;k)	[w-V]	mb event system 3
Def		eventtype(k;loc;V;M;e)	[eventtype]	mb event system 2
Def		valtype(i;a)	[w-valtype]	mb event system 3
Def		msg(a)	[w-msg]	mb event system 3
Def		kindcase(k;a.f(a);l,t.g(l;t))	[kindcase]	mb event system 2
Def		tag(k)	[tagof]	mb event system 2
Def		(e < e')	[es-causl]	mb event system 2
Def		pred(e)	[w-pred]	mb event system 3
Def		first(e)	[w-first]	mb event system 3
Def		(x after e)	[w-after]	mb event system 3
Def		(x when e)	[w-when]	mb event system 3
Def		val(e)	[w-eval]	mb event system 3
Def		kind(e)	[w-ekind]	mb event system 3
Def		w.M	[w-M]	mb event system 3
Def		s(i;t).x	[w-s]	mb event system 3
Def		act(e)	[w-act]	mb event system 3
Def		a(i;t)	[w-a]	mb event system 3
Def		m(i;t)	[w-m]	mb event system 3
Def		val(a)	[w-val]	mb event system 3
Def		mtag(m)	[mtag]	mb event system 1
Def		e <loc e'	[w-locl]	mb event system 3
Def		time(e)	[w-time]	mb event system 3
Def		w.TA	[w-TA]	mb event system 3
Def		2of(t)	[pi2]	core
Def		E	[es-E]	mb event system 2
Def		mlnk(m)	[mlnk]	mb event system 1
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		eqof(d)	[eqof]	mb event system 2
Def		lnk(k)	[lnk]	mb event system 2
Def		loc(e)	[w-loc]	mb event system 3
Def		vartype(i;x)	[w-vartype]	mb event system 3
Def		kind(a)	[w-kind]	mb event system 3
Def		fpf-dom-list(f)	[fpf-dom-list]	mb event system 4
Def		sumdeq(a;b)	[sumdeq]	mb event system 2
Def		w.T	[w-T]	mb event system 3
Def		1of(t)	[pi1]	core
Def		A & B	[cand]	core
Def		x before y  l	[l_before]	mb list 1
Def		Id	[Id]	mb event system 1
Def		SWellFounded(R(x;y))	[strongwellfounded]	mb event system 2
Def			[nat]	int 1
Def		L1  L2	[sublist]	mb list 1
Def		increasing(f;k)	[increasing]	mb basic
Def		{i..j}	[int_seg]	int 1
Def		ij	[ge]	core
Def		i  j < k	[lelt]	int 1
Def		AB	[le]	core
Def		A	[not]	core
Def		null(as)	[null]	list 1
Def		Top	[top]	core
Def		map(f;as)	[map]	list 1
Def		locl(a)	[locl]	mb event system 1
Def		P & Q	[and]	core
Def		x:A. B(x)	[exists]	core
Def		P  Q	[implies]	core
Def		x:A. B(x)	[all]	core
Def			[ma-empty]	mb event system 4
Def		if b t else f fi	[ifthenelse]	bool 1
Def		P  Q	[rev_implies]	core
Def		Surj(A; B; f)	[surject]	fun 1
Def		x : t initially x = v	[ma-single-init]	mb event system 4
Def		only members of L affect x :t	[ma-single-frame]	mb event system 4
Def		only L sends on (l with tg)	[ma-single-sframe]	mb event system 4
Def			[fpf-empty]	mb event system 3
Def		x : v	[fpf-single]	mb event system 4
Def		mk-ma(ds; da; init; pre; ef; send; frame; sframe)	[mk-ma]	mb event system 4
Def		NatDeq	[nat-deq]	mb event system 2
Def		AtomDeq	[atom-deq]	mb event system 2
Def		l[i]	[select]	list 1
Def		||as||	[length]	list 1
Def		1,2. b(1;2)	[so_lambda2]
Def		isrcv(k)	[isrcv]	mb event system 1
Def		isnull(a)	[w-isnull]	mb event system 3
Def		act(k)	[actof]	mb event system 2
Def		islocal(k)	[islocal]	mb event system 1
Def		hd(l)	[hd]	list 1
Def		R^+	[rel_plus]	mb event system 2
Def		R^n	[rel_exp]	mb nat
Def		upto(n)	[upto]	mb event system 1
Def		i=j	[eq_int]	bool 1
Def		x=yAtom	[eq_atom]	bool 1
Def		p  q	[bor]	bool 1
Def		nth_tl(n;as)	[nth_tl]	list 1
Def		ij	[le_int]	bool 1
Def		b	[bnot]	bool 1
Def		as @ bs	[append]	list 1
Def		sum-deq(A;B;a;b)	[sum-deq]	mb event system 2
Def		outl(x)	[outl]	union
Def		isl(x)	[isl]	union
Def		mu(f)	[mu]	mb event system 1
Def		Trans x,y:T. E(x;y)	[trans]	rel 1
Def		outr(x)	[outr]	union
Def		tl(l)	[tl]	list 1
Def			[nat_plus]	int 1
Def		i<j	[lt_int]	bool 1

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