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.