Def		cons	[hcons]
Def		null	[hnull]
Def		tl	[htl]
Def		it_sum	[hit_sum]
Def		append	[happend]
Def		flat	[hflat]
Def		length	[hlength]
Def		map	[hmap]
Def		map2	[hmap2]
Def		every	[hevery]
Def		mt(l)	[mt]
Def		Prop	[prop]	core
Def		x:A. B(x)	[all]	core
Def		P & Q	[and]	core
Def		iso_pair('a;'b;P;rep;abs)	[iso_pair]	hol
Def		type_definition	[htype_definition]	hol bool
Def		type_definition('a;'b;P;rep)	[type_definition]	hol
Def		P  Q	[iff]	core
Def		Dec(P)	[decidable]	core
Def		el	[hel]
Def		hnum	[hnum]	hol num
Def		lt	[hlt]	hol prim rec
Def		is_list_rep	[his_list_rep]
Def		abs_list	[habs_list]
Def		rep_list	[hrep_list]
Def		rep_list('a;l)	[rep_list]
Def			[nat]	int 1
Def		AB	[le]	core
Def		A	[not]	core
Def		P  Q	[implies]	core
Def		select	[hselect]	hol min
Def		exists	[hexists]	hol bool
Def		all	[hall]	hol bool
Def		@x:'a. p(x)	[bchoose]	hol min
Def		x:T. P(x)	[bexists]	hol
Def		x:T. P(x)	[ball]	hol
Def		b	[assert]	bool 1
Def		S	[stype]	hol
Def		hlist('a)	[hlist]
Def		'a  'b	[hfun]	hol min
Def		t	[ht]	hol bool
Def		cond	[hcond]	hol bool
Def		pair	[hpair]	hol pair
Def		hbool	[hbool]	hol min
Def		equal	[hequal]	hol min
Def		hprod('a; 'b)	[hprod]	hol pair
Def		and	[hand]	hol bool
Def		nil	[hnil]
Def		False	[false]	core
Def		True	[true]	core
Def		l[i]	[select]	list 1
Def		it_sum(l)	[it_sum]
Def		flatten(l)	[flatten]
Def		map2(f;l1;l2)	[map2]
Def		hd	[hhd]
Def		every(p;l)	[every]
Def		head(l)	[head]
Def		hd(l)	[hd]	list 1
Def		@x:T. P(x)	[choose]	hol
Def		arb(T)	[arb]	hol
Def		||as||	[length]	list 1
Def		nth_tl(n;as)	[nth_tl]	list 1
Def		ij	[le_int]	bool 1
Def		i<j	[lt_int]	bool 1
Def		bif(b; bx.x(bx); by.y(by))	[bif]	hol
Def		x:T. b(x)	[tlambda]	fun 1
Def		tl(l)	[tl]	list 1
Def		null(as)	[null]	list 1
Def		Y	[ycomb]	core
Def		as @ bs	[append]	list 1
Def		pq	[band]	bool 1
Def		true	[btrue]	bool 1
Def		x = y	[bequal]	hol
Def		map(f;as)	[map]	list 1
Def		i=j	[eq_int]	bool 1
Def			[bool]	bool 1
Def		P  Q	[rev_implies]	core
Def		P	[prop_to_bool]	hol
Def		b	[bnot]	bool 1

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