About this site
This site is an experimental HTML rendering of fragments of the IsarMathLib project. IsarMathLib is a library of mathematical proofs formally verified by the Isabelle theorem proving environment. The formalization is based on the Zermelo-Fraenkel set theory. The Introduction provides more information about IsarMathLib.
The software for exporting Isabelle's Isar language to HTML markup is at an early beta stage, so some proofs may be rendered incorrectly. In case of doubts, compare with the Isabelle generated HTML presentation, the proof document or directly the theory sources.
Mathematical notation on this site is rendered by MathJax. MathJax is an implementation of TeX layout algorithms in JavaScript. After loading a page you may see the LaTeX markup instead of mathematical notation for a second or two before MathJax script renders the math symbols.
