diff -r c799d0859638 -r cc778d613217 src/HOL/Isar_examples/README.html
--- /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 @@
+
+
+
+
+HOL/Isar_examples
+
+
+
+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.
+
+
+