Def		sexprAtom(s)	[sfa_doc_sexpr_atom]
Def		x:A. B(x)	[sfa_doc_sigma_notation]
Def		x:A. B(x)	[sfa_doc_pi_notation]
Def		max(a;b)	[sfa_doc_max_int]
Def		i steps of e from a	[sfa_doc_sequence_rel]
Def			[int_nzero]	int 1
Def		a  b	[nequal]	core
Def		f zero beyond x	[sfa_doc_props_as_types_example1]
Def		u in X: A^n. P(u)	[sfa_doc_ntuple_contains]
Def		ij	[ge]	core
Def		y greater-bounds x	[sfa_doc_greater_list_bound]
Def		{i..j}	[int_seg]	int 1
Def		Induction for x:. P(x)	[sfa_doc_indscheme]
Def		sfa_doc_oparm_sample{2:n} sfa_doc_oparm_sample(A)	[sfa_doc_oparm_sample2]
Def		sfa_doc_oparm_sample{1:n} sfa_doc_oparm_sample(A)	[sfa_doc_oparm_sample1]
Def			[nat]	int 1
Def		{i...j}	[int_iseg]	int 1
Def		i  j < k	[lelt]	int 1
Def		AB	[le]	core
Def		Dec(P)	[decidable]	core
Def		A	[not]	core
Def		A =ext B	[sfa_doc_exteq]
Def		sexprCar(s)	[sfa_doc_sexpr_car]
Def		sexprCdr(s)	[sfa_doc_sexpr_cdr]
Def		P  Q	[iff]	core
Def		{T}	[guard]	core
Def		i even	[sfa_doc_even]
Def		a list xs	[sfa_doc_inlist]
Def		{a:T}	[singleton]	core
Def		f{m..n}	[listify]	list 1
Def		l[i]	[select]	list 1
Def		||as||	[length]	list 1
Def		pq	[band]	bool 1
Def		b	[assert]	bool 1
Def		if b t else f fi	[ifthenelse]	bool 1
Def		false	[bfalse]	bool 1
Def		true	[btrue]	bool 1
Def			[bool]	bool 1
Def			[it]	core
Def		Unit	[unit]	core
Def			[nat_plus]	int 1
Def		nth_tl(n;as)	[nth_tl]	list 1
Def		ij	[le_int]	bool 1
Def		i<j	[lt_int]	bool 1
Def		A^n	[sfa_doc_ntuple]
Def		x!	[sfa_doc_factorial2]
Def		x!	[sfa_doc_factorial]
Def		i=j	[eq_int]	bool 1
Def		x=yAtom	[eq_atom]	bool 1
Def		outr(x)	[outr]	union
Def		outl(x)	[outl]	union
Def		isl(x)	[isl]	union
Def		rev(as)	[reverse]	list 1
Def		mod k	[sfa_doc_sample_intmod]
Def		mu	[kleene_minimize]
Def		Y	[ycomb]	core
Def		Reverse(e)	[sfa_doc_sexpr_reverse]
Def		Size(s)	[sfa_doc_sexpr_size]
Def		Case of s :  Inj(x)  g(x) ; Cons(s1;s2)  f(s1;s2)	[sfa_doc_sexpr_cases]
Def		Inj(a)	[sfa_doc_sexpr_inj]
Def		Cons(s1;s2)	[sfa_doc_sexpr_cons]
Def		Sexpr(A)	[sfa_doc_sexpr]
Def		t  T	[member]
Def		HigherConsequence{i}(P)	[sfa_doc_le_parm_sample_def]
Def		f o g	[compose]	fun 1
Def		$abc.$n	[sfa_doc_tok_num_literal]
Def		Weird(x; u,v. F(u;v))	[sfa_doc_weird_def]
Def		Sym x,y:T. E(x;y)	[sym]	rel 1
Def		x:A. B(x)	[exists]	core
Def		x:A. B(x)	[all]	core
Def		True	[true]	core
Def		False	[false]	core
Def		P  Q	[or]	core
Def		P & Q	[and]	core
Def		P  Q	[implies]	core
Def		map(f;as)	[map]	list 1
Def		Prop	[prop]	core
Def		SQType(T)	[sq_type]	sqequal 1
Def		Top	[top]	core
Def		S  T	[subtype]	core
Def		P  Q	[rev_implies]	core
Def		hd(l)	[hd]	list 1
Def		b	[bnot]	bool 1
Def		as @ bs	[append]	list 1
Def		tl(l)	[tl]	list 1

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