--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Isar_Examples/README.html Tue Oct 20 19:37:09 2009 +0200
@@ -0,0 +1,21 @@
+<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
+
+<!-- $Id$ -->
+
+<html>
+
+<head>
+ <meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1">
+ <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
+also the included document, or the <a
+href="http://isabelle.in.tum.de/Isar/">Isabelle/Isar page</a> for more
+information.
+</body>
+</html>