Def		a +q b	[qadd]
Def			[rat]
Def		x:A. B(x)	[all]	core
Def		a *q b	[qmul]
Def		a =q b	[eq_rat]
Def		b	[assert]	bool 1
Def		P  Q	[implies]	core
Def			[nat_plus]	int 1
Def		q.num	[qnumer]
Def		1of(t)	[pi1]	core
Def		q.den	[qdenom]
Def		2of(t)	[pi2]	core
Def		i=j	[eq_int]	bool 1
Def		p/q	[qnum]

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