This appendix contains some of the theory files for the development of nonstandard analysis described in the paper Mechanizing nonstandard real analysis.
The files should be used with Isabelle99, the current release of the theorem-prover.
As this work evolves, up-to-date versions of the theory files will be available in the online Isabelle distribution.
The files contained are: