<!-- $Id$ -->
<html>
<head>
<title>HOL/Isar_examples</title>
</head>
<body>
<h1>HOL/Isar_examples</h1>
Isar offers a new high-level proof (and theory) language interface to
Isabelle. This directory contains some example Isar documents. See
the <a href="http://isabelle.in.tum.de/Isar/">Isabelle/Isar page</a>
for more information.
<p>
Note that the theory files are basically just plain ASCII sources of
what are meant to be actual typeset documents. Automatic LaTeX / PDF
pretty printing will be available in the near future.
<body>
</html>