Definitions PrimesSquareRoots DiscrMathExt Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Defined Operators mentioned in PrimesSquareRoots

Def  prime(a)[prime]num thy 1
Def  a ~ b[assoced]num thy 1
Def  b | a[divides]num thy 1
Def  P  Q[iff]core
Def  P  Q[implies]core
Def  x:AB(x)[all]core
Def  [nat]int 1
Def  AB[le]core
Def  A[not]core
Def  P & Q[and]core
Def  x:AB(x)[exists]core
Def  Prop[prop]core
Def  [nat_plus]int 1
Def  P  Q[rev_implies]core

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

Definitions PrimesSquareRoots DiscrMathExt Doc