This paper describes the theory of design and implementation of an interactive theorem prover for the differential and integral calculus in one variable. Up to now, nonstandard infinitesimal analysis has been used mainly for proofs. We believe there is a natural affinity between infinitesimals and the extensive use of computational arguments which has not been exploited enough. This is a preliminary version of the system that will be developed and only covers the first part of the work presented in the work of Chuaqui and Suppes including theorems on the differential calculus. Once finished it will be better than any symbolic manipulation program that solves algebraic, differentiation, and integration problems automatically, because of its ``transparency'', and by the fact that it will include all the conditions for the solutions to be valid. Thus, it may be used both by mathematicians and by those who apply mathematics, such as physicists, engineers, and economists.