I-SMALL

ACL2(r) recognizer for infinitesimal numbers 
Major Section:  REAL

(I-small x) is true if and only if x is an infinitesimal number (possibly 0). This predicate is only defined in ACL2(r) (see real).