--- a/src/HOL/Isar_examples/BasicLogic.thy Wed Jul 14 13:06:08 1999 +0200
+++ b/src/HOL/Isar_examples/BasicLogic.thy Wed Jul 14 13:07:09 1999 +0200
@@ -27,7 +27,7 @@
qed;
lemma K': "A --> B --> A";
-proof single+; txt {* better use sufficient-to-show here \dots *};
+proof single+ -- {* better use sufficient-to-show here \dots *};
assume A;
show A; .;
qed;
--- a/src/HOL/Isar_examples/Group.thy Wed Jul 14 13:06:08 1999 +0200
+++ b/src/HOL/Isar_examples/Group.thy Wed Jul 14 13:07:09 1999 +0200
@@ -128,7 +128,7 @@
monoid_right_unit: "x * one = x";
text {*
- Groups are *not* yet monoids directly from the definition . For
+ Groups are *not* yet monoids directly from the definition. For
monoids, right_unit had to be included as an axiom, but for groups
both right_unit and right_inverse are derivable from the other
axioms. With group_right_unit derived as a theorem of group theory
--- /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>