Nuprl - Some Definitions

Thms bool 1 Doc

nequal	`Def abT == a = b T` `Thm* x,y:A. xy Prop`
not	`Def A == A False` `Thm* (A) Prop`
iff	`Def P Q == (P Q) & (P Q)` `Thm* (A B) Prop`
rev_implies	`Def P Q == Q P` `Thm* (A B) Prop`