Def		prod-deq-aux{\\\\v:l,i:l}(A;B;a;b)	[prod-deq-aux]
Def		sum-deq-aux{\\\\v:l,i:l}(A;B;a;b)	[sum-deq-aux]
Def		DS(A)	[discrete_struct]
Def		dstype(TypeNames; d; a)	[dstype]
Def		event_system_typename()	[event_system_typename]
Def		mk-es(E; eq; T; V; M; loc; k; v; w; a; snds; sndr; i; f; prd; cl; p)	[mk-es]
Def		true	[btrue]	bool 1
Def		strong-subtype(A;B)	[strong-subtype]	mb event system 1
Def		(x  l)	[l_member]	mb list 1
Def		deq-member(eq;x;L)	[deq-member]
Def		Dec(P)	[decidable]	core
Def		a = b	[eq_lnk]
Def		lconnects(p;i;j)	[lconnects]
Def		l_interval(l;j;i)	[l_interval]	mb event system 1
Def		a = b	[eq_knd]
Def		has-src(i;k)	[has-src]
Def		WellFnd{i}(A;x,y.R(x;y))	[wellfounded]	well fnd
Def		R^+	[rel_plus]
Def		ES	[event_system]
Def		e = e'	[es-eq-E]
Def		(Msg on l)	[es-Msgl]
Def		valtype(e)	[es-valtype]
Def		vartype(i;x)	[es-vartype]
Def		val(e)	[es-val]
Def		(x when e)	[es-when]
Def		(x after e)	[es-after]
Def		sends(l;e)	[es-sends]
Def		sender(e)	[es-sender]
Def		index(e)	[es-index]
Def		first(e)	[es-first]
Def		pred(e)	[es-pred]
Def		e  e'	[es-le]
Def		{T}	[guard]	core
Def		rcv(l; tg)	[rcv]	mb event system 1
Def		eventtype(k;loc;V;M;e)	[eventtype]
Def		kindcase(k;a.f(a);l,t.g(l;t))	[kindcase]
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]
Def		rcvtype(e)	[es-rcvtype]
Def		tag(e)	[es-tag]
Def		tag(k)	[tagof]
Def		lnk(e)	[es-lnk]
Def		lnk(k)	[lnk]
Def		outl(x)	[outl]	union
Def		lpath(p)	[lpath]
Def		source(l)	[lsrc]
Def		a = b	[eq_id]
Def		KindDeq	[Kind-deq]
Def		IdLnkDeq	[idlnk-deq]
Def		IdDeq	[id-deq]
Def		product-deq(A;B;a;b)	[product-deq]
Def		proddeq(a;b)	[proddeq]
Def		union-deq(A;B;a;b)	[union-deq]
Def		sumdeq(a;b)	[sumdeq]
Def		eqof(d)	[eqof]
Def		lnk-inv(l)	[lnk-inv]	mb event system 1
Def		destination(l)	[ldst]
Def		Msg_sub(l; M)	[Msg_sub]	mb event system 1
Def		haslink(l; m)	[haslink]	mb event system 1
Def		Msg	[es-Msg]
Def		acttype(e)	[es-acttype]
Def		act(e)	[es-act]
Def		isrcv(e)	[es-isrcv]
Def		kind(e)	[es-kind]
Def		(e <loc e')	[es-locl]
Def		loc(e)	[es-loc]
Def		(e < e')	[es-causl]
Def		E	[es-E]
Def		mlnk(m)	[mlnk]	mb event system 1
Def		1of(t)	[pi1]	core
Def		2of(t)	[pi2]	core
Def		act(k)	[actof]
Def		outr(x)	[outr]	union
Def		islocal(k)	[islocal]	mb event system 1
Def		if b t else f fi	[ifthenelse]	bool 1
Def		isrcv(k)	[isrcv]	mb event system 1
Def		prod-deq(A;B;a;b)	[prod-deq]
Def		pq	[band]	bool 1
Def		EqDecider(T)	[deq]
Def		b	[assert]	bool 1
Def		P  Q	[iff]	core
Def		x:A. B(x)	[all]	core
Def			[bool]	bool 1
Def		NatDeq	[nat-deq]
Def		R^n	[rel_exp]	mb nat
Def		mklist(n;f)	[mklist]	mb list 1
Def		primrec(n;b;c)	[primrec]	mb nat
Def		i=j	[eq_int]	bool 1
Def		AtomDeq	[atom-deq]
Def		x=yAtom	[eq_atom]	bool 1
Def		P & Q	[and]	core
Def		false	[bfalse]	bool 1
Def		sum-deq(A;B;a;b)	[sum-deq]
Def		p  q	[bor]	bool 1
Def		reduce(f;k;as)	[reduce]	list 1
Def		Msg(M)	[Msg]	mb event system 1
Def		Knd	[Knd]	mb event system 1
Def		IdLnk	[IdLnk]	mb event system 1
Def		Id	[Id]	mb event system 1
Def		SWellFounded(R(x;y))	[strongwellfounded]
Def			[nat]	int 1
Def		{i..j}	[int_seg]	int 1
Def		i  j < k	[lelt]	int 1
Def		AB	[le]	core
Def		A	[not]	core
Def		last(L)	[last]	mb list 1
Def		l[i]	[select]	list 1
Def		||as||	[length]	list 1
Def		hd(l)	[hd]	list 1
Def		P  Q	[implies]	core
Def		x:A. B(x)	[exists]	core
Def		x f y	[infix_ap]	core
Def			[nat_plus]	int 1
Def		A & B	[cand]	core
Def		Trans x,y:T. E(x;y)	[trans]	rel 1
Def		P  Q	[or]	core
Def		Prop	[prop]	core
Def		Top	[top]	core
Def			[it]	core
Def		isl(x)	[isl]	union
Def		nth_tl(n;as)	[nth_tl]	list 1
Def		ij	[le_int]	bool 1
Def		b	[bnot]	bool 1
Def		P  Q	[rev_implies]	core
Def		as @ bs	[append]	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