Def		zero	[hzero]	hol num
Def		A[P]	[type_if]	hol
Def		type_tag(x;'a)	[type_tag]	hol
Def		type_definition	[htype_definition]	hol bool
Def		hbool	[hbool]	hol min
Def		hone	[hone]	hol one
Def		exists	[hexists]	hol bool
Def		t	[ht]	hol bool
Def		select	[hselect]	hol min
Def		one_el	[hone_el]	hol one
Def		equal	[hequal]	hol min
Def		all	[hall]	hol bool
Def		S	[stype]	hol
Def		exists_unique	[hexists_unique]	hol bool
Def		P  Q	[or]	core
Def		suc	[hsuc]	hol num
Def		add	[hadd]	hol arithmetic 1
Def		lt	[hlt]	hol prim rec
Def		sub	[hsub]	hol arithmetic 1
Def		mult	[hmult]	hol arithmetic 1
Def		exp	[hexp]	hol arithmetic 1
Def		gt	[hgt]	hol arithmetic 1
Def		le	[hle]	hol arithmetic 1
Def		ge	[hge]	hol arithmetic 1
Def		fact	[hfact]	hol arithmetic 1
Def		even	[heven]	hol arithmetic 1
Def		odd	[hodd]	hol arithmetic 1
Def		mod	[hmod]	hol arithmetic 1
Def		div	[hdiv]	hol arithmetic 1
Def		pre	[hpre]	hol prim rec
Def		rep_list	[hrep_list]	hol list 1
Def		abs_list	[habs_list]	hol list 1
Def		it_sum	[hit_sum]	hol list 1
Def		el	[hel]	hol list 1
Def		is_list_rep	[his_list_rep]	hol list 1
Def		simp_rec_fun	[hsimp_rec_fun]	hol prim rec
Def		prim_rec	[hprim_rec]	hol prim rec
Def		abs_num	[habs_num]	hol num
Def		hind	[hind]	hol min
Def		is_num_rep	[his_num_rep]	hol num
Def		rep_list('a;l)	[rep_list]	hol list 1
Def		simp_rec_rel	[hsimp_rec_rel]	hol prim rec
Def		prim_rec_fun	[hprim_rec_fun]	hol prim rec
Def		hnum	[hnum]	hol num
Def		simp_rec	[hsimp_rec]	hol prim rec
Def		rep_num	[hrep_num]	hol num
Def		zero_rep	[hzero_rep]	hol num
Def		suc_rep	[hsuc_rep]	hol num
Def			[nat]	int 1
Def		AB	[le]	core
Def		and	[hand]	hol bool
Def		cond	[hcond]	hol bool
Def		or	[hor]	hol bool
Def		not	[hnot]	hol bool
Def		f	[hf]	hol bool
Def		implies	[himplies]	hol min
Def		snd	[hsnd]	hol pair
Def		fst	[hfst]	hol pair
Def		pair	[hpair]	hol pair
Def		cons	[hcons]	hol list 1
Def		hlist('a)	[hlist]	hol list 1
Def		nil	[hnil]	hol list 1
Def		null	[hnull]	hol list 1
Def		tl	[htl]	hol list 1
Def		append	[happend]	hol list 1
Def		flat	[hflat]	hol list 1
Def		length	[hlength]	hol list 1
Def		map	[hmap]	hol list 1
Def		map2	[hmap2]	hol list 1
Def		every	[hevery]	hol list 1
Def		mt(l)	[mt]	hol list 1
Def		Prop	[prop]	core
Def		XM	[xmiddle]	core
Def		Dec(P)	[decidable]	core
Def		hprod('a; 'b)	[hprod]	hol pair
Def		iso_pair('a;'b;P;rep;abs)	[iso_pair]	hol
Def		res_forall	[hres_forall]	hol restr binder
Def		res_exists	[hres_exists]	hol restr binder
Def		res_select	[hres_select]	hol restr binder
Def		arb	[harb]	hol restr binder
Def		res_abstract	[hres_abstract]	hol restr binder
Def		i>j	[gt]	core
Def		curry	[hcurry]	hol pair
Def		is_pair	[his_pair]	hol pair
Def		rep_prod	[hrep_prod]	hol pair
Def		uncurry	[huncurry]	hol pair
Def		onto	[honto]	hol bool
Def		one_one	[hone_one]	hol bool
Def		{T}	[guard]	core
Def		outl(x)	[outl]	union
Def		outl	[houtl]	hol sum
Def		outr(x)	[outr]	union
Def		outr	[houtr]	hol sum
Def		hsum('a; 'b)	[hsum]	hol sum
Def		is_sum_rep	[his_sum_rep]	hol sum
Def		abs_sum	[habs_sum]	hol sum
Def		inl	[hinl]	hol sum
Def		inr	[hinr]	hol sum
Def		isl	[hisl]	hol sum
Def		isr	[hisr]	hol sum
Def		o	[ho]	hol combin
Def		k	[hk]	hol combin
Def		s	[hs]	hol combin
Def		i	[hi]	hol combin
Def		let	[hlet]	hol bool
Def		P	[prop_to_bool_2]	hol
Def		eq('a)	[eq_pred]	hol
Def		S  T	[subtype]	core
Def		<eq_pred:x>	[eq_pred_marker]	hol
Def		Unit	[unit]	core
Def			[it]	core
Def		False	[false]	core
Def		True	[true]	core
Def		l[i]	[select]	list 1
Def		it_sum(l)	[it_sum]	hol list 1
Def		flatten(l)	[flatten]	hol list 1
Def		map2(f;l1;l2)	[map2]	hol list 1
Def		hd	[hhd]	hol list 1
Def		every(p;l)	[every]	hol list 1
Def		head(l)	[head]	hol list 1
Def		hd(l)	[hd]	list 1
Def		@x:'a. p(x)	[bchoose]	hol min
Def		res_choose('a;x.P(x);x.Q(x))	[res_choose]	hol restr binder
Def		@x:T. P(x)	[choose]	hol
Def		res_lambda('a;'b;x.P(x);x.f(x))	[res_lambda]	hol restr binder
Def		arb(T)	[arb]	hol
Def		||as||	[length]	list 1
Def		nnsub(m;n)	[nnsub]	hol arithmetic 1
Def		nth_tl(n;as)	[nth_tl]	list 1
Def		ij	[le_int]	bool 1
Def		i<j	[lt_int]	bool 1
Def		exp(m;n)	[exp]	hol arithmetic 1
Def		fact(n)	[fact]	hol arithmetic 1
Def		even(n)	[even]	hol arithmetic 1
Def		odd(n)	[odd]	hol arithmetic 1
Def		nmod(m;n)	[nmod]	hol arithmetic 1
Def		ndiv(m;n)	[ndiv]	hol arithmetic 1
Def		ncompose(f;n;x)	[ncompose]	hol num
Def		pre(n)	[pre]	hol prim rec
Def		bif(b; bx.x(bx); by.y(by))	[bif]	hol
Def		mk_pair	[hmk_pair]	hol pair
Def		rep_sum	[hrep_sum]	hol sum
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		b_exists_unique('a;x.p(x))	[b_exists_unique]	hol bool
Def		pq	[band]	bool 1
Def		true	[btrue]	bool 1
Def		x = y	[bequal]	hol
Def		x:T. P(x)	[bexists]	hol
Def		map(f;as)	[map]	list 1
Def		i=j	[eq_int]	bool 1
Def			[bool]	bool 1
Def		P  Q	[implies]	core
Def		x:A. B(x)	[all]	core
Def		P & Q	[and]	core
Def		x:A. B(x)	[exists]	core
Def		x:T. P(x)	[ball]	hol
Def		type_definition('a;'b;P;rep)	[type_definition]	hol
Def		b	[assert]	bool 1
Def		res_all('a;x.P(x);x.Q(x))	[res_all]	hol restr binder
Def		P	[prop_to_bool]	hol
Def		res_exists('a;x.P(x);x.Q(x))	[res_exists]	hol restr binder
Def		pq	[bimplies]	bool 1
Def		b	[bnot]	bool 1
Def		false	[bfalse]	bool 1
Def		'a  'b	[hfun]	hol min
Def		2of(t)	[pi2]	core
Def		1of(t)	[pi1]	core
Def		onto('a;'b;f)	[onto]	hol bool
Def		A	[not]	core
Def		one_one('a;'b;f)	[one_one]	hol bool
Def		if b t else f fi	[ifthenelse]	bool 1
Def		isl(x)	[isl]	union
Def		isr(x)	[isr]	hol
Def		f o g	[compose]	fun 1
Def		p  q	[bor]	bool 1
Def		let x = a in b(x)	[let]	core
Def		P  Q	[iff]	core
Def		P  Q	[rev_implies]	core

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