Def		EquivRel on A, R	[equiv_rel_sep]	LogicSupplement
Def		Q(x)	[allst_implicit]	LogicSupplement
Def		x:A. B(x)	[product_conventional_notation]	LogicSupplement
Def		A/E	[quotient_sep]	LogicSupplement
Def		AB	[isect_two]	LogicSupplement
Def		x:A st P(x)B(x)	[fun_over_st]	LogicSupplement
Def		let xa in b(x)	[pure_let]	LogicSupplement
Def		let xa, yb in c(x;y)	[pure_let2]	LogicSupplement
Def		f is a factorization of k	[prime_factorization_of]	FTA
Def		is_prime_factorization(a; b; f)	[is_prime_factorization]	FTA
Def		Prime	[prime_nats]	SimpleMulFacts
Def		prime(a)	[prime]	num thy 1
Def		a ~ b	[assoced]	num thy 1
Def		b | a	[divides]	num thy 1
Def		IsEqFun(T;eq)	[eqfun_p]	rel 1
Def		P  Q	[iff]	core
Def		Prop	[prop]	core
Def			[nat_plus]	int 1
Def		{T}	[guard]	core
Def		{i...}	[int_upper]	int 1
Def		{i..j}	[int_seg]	int 1
Def		i  j < k	[lelt]	int 1
Def			[nat]	int 1
Def		AB	[le]	core
Def		trivial_factorization(z)	[trivial_factorization]	FTA
Def			[int_nzero]	int 1
Def		a  b	[nequal]	core
Def		reduce_factorization(f; j)	[reduce_factorization]	FTA
Def		SqStable(P)	[sq_stable]	core
Def		A & B	[cand]	core
Def		split_factor2(g; x; y)	[split_factor2]	FTA
Def		split_factor1(g; x)	[split_factor1]	FTA
Def			[bool]	bool 1
Def		b	[assert]	bool 1
Def		complete_intseg_mset(a; b; f)	[complete_intseg_mset]	FTA
Def		!x:A. P(x)	[exists_unique]	LogicSupplement
Def		{a:T}	[singleton]	core
Def		A =ext B	[exteq]	LogicSupplement
Def		!A	[inhabited_uniquely]	LogicSupplement
Def		S  T	[subtype]	core
Def		A Discrete	[is_discrete]	LogicSupplement
Def		x f y	[infix_ap]	core
Def		T	[squash]	core
Def		True	[true]	core
Def		P XOR Q	[xor]	LogicSupplement
Def		Diag f wrt y. e(y)	[diagonalize]	LogicSupplement
Def		prime_mset_complete(f)	[prime_mset_complete]	FTA
Def		is_prime(x)	[prime_decider]	SimpleMulFacts
Def		if b t else f fi	[ifthenelse]	bool 1
Def		{a..b}(f)	[eval_factorization]	FTA
Def		Iter(f;u) i:{a..b}. e(i)	[iter_via_intseg]	IteratedBinops
Def		P  Q	[implies]	core
Def		x:A. B(x)	[all]	core
Def		P & Q	[and]	core
Def		i=j	[eq_int]	bool 1
Def		i  j < k	[lelt_int]	FTA
Def		ij	[le_int]	bool 1
Def		i<j	[lt_int]	bool 1
Def		pq	[band]	bool 1
Def		P  Q	[or]	core
Def		x:A. B(x)	[exists]	core
Def		A	[inhabited]	LogicSupplement
Def		Dec(P)	[decidable]	core
Def		A	[not]	core
Def		EquivRel x,y:T. E(x;y)	[equiv_rel]	rel 1
Def		x:A st P(x). Q(x)	[allst]	LogicSupplement
Def		x is the u:A. P(u)	[is_the]	LogicSupplement
Def		P  Q	[rev_implies]	core
Def		b	[bnot]	bool 1
Def		Trans x,y:T. E(x;y)	[trans]	rel 1
Def		Sym x,y:T. E(x;y)	[sym]	rel 1
Def		Refl(T;x,y.E(x;y))	[refl]	rel 1

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