At first glance, Robinson's original form of nonstandard analysis appears nonconstructive in essence, because it makes a rather unrestricted use of classical logic and set theory and, in particular, of the axiom of choice.