Def		Default => body EndSwitch	[switch_default]
Def		Case(value) body	[case]
Def		Default => body	[case_default]
Def		<x,y> => <x,ybody(x;y)	[case_pair]
Def		inl(x) => inl(body(x) cont	[case_inl]
Def		inr(x) => inr(body(x) cont	[case_inr]
Def		x::y => x::ybody(x;y) cont	[case_cons]
Def		[] => [] =body cont	[case_nil]
Def		=>  =>body	[case_it]
Def		x:body	[case_bind]
Def		<<"a", b>, c, 1> => <<"abody(b;c) cont	[case_pattern1]
Def		<a, inl <<"a", b>, c, 1>> => <a, body(a;b;c) cont	[case_pattern2]
Def		<a, inl <<"a", b>, c, 1>>	[pattern2]
Def		union1()	[union1]
Def		union1_term1(x) => uniobody(x) cont	[case_union1_term1]
Def		union1_term1(x)	[union1_term1]
Def		union1_term2(x) => uniobody(x) cont	[case_union1_term2]
Def		union1_term2(x)	[union1_term2]
Def		union1_term3(x) => uniobody(x) cont	[case_union1_term3]
Def		union1_term3(x)	[union1_term3]
Def		enum1_switch(value;el1;el2;el3)	[enum1_switch]
Def		enum1_el1 => enumbody cont	[case_enum1_el1]
Def		enum1_el2 => enumbody cont	[case_enum1_el2]
Def		enum1_el3 => enumbody cont	[case_enum1_el3]
Def		module1_type(prop)	[module1_type]
Def		t.tag	[module1_tag]
Def		t.data	[module1_data]
Def		module1(tag, data) => modubody(tag;data)	[case_module1]
Def		module1(tag, data)	[module1]
Def		enum1()	[enum1]
Def		SQType(T)	[sq_type]	sqequal 1
Def		true	[btrue]	bool 1
Def		P  Q	[implies]	core
Def		x:A. B(x)	[all]	core
Def		false	[bfalse]	bool 1
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		P  Q	[or]	core
Def		Case v => case cont	[switch_case]
Def		i=j	[eq_int]	bool 1
Def		if b t else f fi	[ifthenelse]	bool 1
Def		<<"a", b>, c, 1>	[pattern1]
Def			[bool]	bool 1
Def		EndSwitch	[switch_done]
Def		enum1_el3	[enum1_el3]
Def		enum1_el2	[enum1_el2]
Def		enum1_el1	[enum1_el1]
Def		Switch(t) b	[switch]
Def		Unit	[unit]	core
Def		Y	[ycomb]	core
Def		1of(t)	[pi1]	core
Def		2of(t)	[pi2]	core

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