%% This BibTeX bibliography file was created using BibDesk.
%% http://bibdesk.sourceforge.net/


%% Created for Larry Paulson at 2022-03-24 16:13:30 +0000 


%% Saved with string encoding Unicode (UTF-8) 



@book{gleason-fundamentals,
	author = {Andrew Gleason},
	booktitle = {Fundamentals of Abstract Analysis },
	date-added = {2022-03-24 16:13:29 +0000},
	date-modified = {2022-03-24 16:13:29 +0000},
	publisher = {Taylor \& Francis},
	title = {Fundamentals of Abstract Analysis },
	year = {1991}}

@phdthesis{jutting77,
	author = {{L.S. van Benthem} Jutting},
	date-added = {2022-03-24 16:03:26 +0000},
	date-modified = {2022-03-24 16:03:26 +0000},
	doi = {https://doi.org/10.6100/IR23183},
	note = {\url{https://doi.org/10.6100/IR23183}},
	school = {Eindhoven University of Technology},
	title = {Checking {Landau's} ``{Grundlagen}'' in the {AUTOMATH} System},
	year = {1977},
	bdsk-url-1 = {https://doi.org/10.6100/IR23183}}

@article{fleuriot-jcm,
	author = {Jacques D. Fleuriot and Lawrence C. Paulson},
	date-added = {2022-03-24 15:42:35 +0000},
	date-modified = {2022-03-24 15:42:35 +0000},
	journal = {LMS Journal of Computation and Mathematics},
	note = {\url{http://www.lms.ac.uk/jcm/3/lms1999-027/}},
	pages = {140-190},
	title = {Mechanizing Nonstandard Real Analysis},
	volume = {3},
	year = {2000}}

@inproceedings{fleuriot-real-analysis,
	abstract = {Our recent, and still ongoing, development of real analysis in Isabelle/HOL is presented and compared, whenever instructive, to the one present in the theorem prover HOL. While most existing mechanizations of analysis only use the classical є and $\delta$ approach, ours uses notions from both Nonstandard Analysis and classical analysis. The overall result is an intuitive, yet rigorous, development of real analysis, and a relatively high degree of proof automation in many cases.},
	author = {Fleuriot, Jacques D.},
	booktitle = {Theorem Proving in Higher Order Logics},
	date-added = {2022-03-24 15:42:12 +0000},
	date-modified = {2022-03-24 15:42:12 +0000},
	editor = {Aagaard, Mark and Harrison, John},
	isbn = {978-3-540-44659-0},
	pages = {145-161},
	publisher = {Springer},
	title = {On the Mechanization of Real Analysis in {Isabelle/HOL}},
	volume = {LNCS 1869},
	year = {2000}}
