Def			[bool]	bool 1
Def		{i...}	[int_upper]	int 1
Def		permute(p to r ; q to s)	[hanoi_peg_perm]
Def			[nat]	int 1
Def		s is a Hanoi(n disk) seq on a..z	[hanoi_seq]
Def		Moving disk k of n takes f to g	[hanoi_step_at]
Def		Peg	[hanoi_PEG]
Def		{i...j}	[int_iseg]	int 1
Def		AB	[le]	core
Def		Prop	[prop]	core
Def			[nat_plus]	int 1
Def		n^k	[exponentiation]
Def		1of(t)	[pi1]	core
Def		false	[bfalse]	bool 1
Def		true	[btrue]	bool 1
Def		p=q	[eq_hanoi_PEG]
Def		if b t else f fi	[ifthenelse]	bool 1
Def		HanoiSTD(n disks; from: p; to: q; indexing from: a)	[hanoi_sol2_ala_generalPROG]
Def		HanoiHelper(n; s1; f; s2; g)	[hanoi_general_exists_lemma2PROG]
Def		s(?) {to n}  h {to n'}	[hanoi_seq_deepen]
Def		f {to n}  f' {to n'}	[hanoi_extend]
Def		s1 @(m) s2	[hanoi_seq_join]
Def		ij	[le_int]	bool 1
Def		a  b	[nequal]	core
Def		P  Q	[iff]	core
Def		x:A. B(x)	[all]	core
Def		P & Q	[and]	core
Def		x:A. B(x)	[exists]	core
Def		P  Q	[implies]	core
Def		i=j	[eq_int]	bool 1
Def		Y	[ycomb]	core
Def		otherPeg(x; y)	[hanoi_otherpeg]
Def		Inj(A; B; f)	[inject]	fun 1
Def		A	[not]	core
Def		i<j	[lt_int]	bool 1
Def		b	[bnot]	bool 1
Def		P  Q	[rev_implies]	core

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