# HG changeset patch
# User wenzelm
# Date 931950429 -7200
# Node ID cc778d613217b99ca2866eb509b26fb986ab8512
# Parent c799d0859638ee343390ced864279fdda17df525
tuned comments;
diff -r c799d0859638 -r cc778d613217 src/HOL/Isar_examples/BasicLogic.thy
--- 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;
diff -r c799d0859638 -r cc778d613217 src/HOL/Isar_examples/Group.thy
--- 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
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.
+
+
+