HOL/Isar_examples

Isar offers a new high-level proof (and theory) language interface to Isabelle. This directory contains some example Isar documents. See the Isabelle/Isar page for more information.

Note that the theory files are basically the plain ASCII sources of what is meant to be actual typeset documents. Automatic LaTeX / PDF pretty printing is not yet available.