--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Isar_examples/README.html	Wed Jul 14 13:07:09 1999 +0200
@@ -0,0 +1,23 @@
+<!-- $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 the plain ASCII sources of
+what is meant to be actual typeset documents.  Automatic LaTeX / PDF
+pretty printing is not yet available.
+
+<body>
+</html>