# Re: [isabelle] Where to learn about HOL vs FOL?

Isabelle has been developed over nearly 30 years, but with largely the same formalism; the only real changes have concerned polymorphism and type classes. Thanks to the LCF architecture, only a tiny percentage of the code has to be trusted. There are papers concerning formal properties of the basic calculus and some of its extensions, which should answer many specific questions. I would mention in particular the following papers:
L. C. Paulson.
The foundation of a generic theorem prover. J. Automated Reasoning 5 (1989), 363–397.
http://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-130.html
Markus Wenzel
Type classes and overloading in higher-order logic
Theorem Proving in Higher Order Logics
Lecture Notes in Computer Science Volume 1275, 1997, pp 307-322
http://www4.in.tum.de/~wenzelm/papers/axclass-TPHOLs97.pdf
Larry Paulson
On 4 Feb 2013, at 22:37, Steven Ericsson-Zenith <steven at iase.us> wrote:
> I'd say from the point of view of constructing real proofs this inaccessibility is a real problem. Are there proof statements concerning the formal properties of Isabelle?
>
> Steven

*This archive was generated by a fusion of
Pipermail (Mailman edition) and
MHonArc.*