tuned comments;
authorwenzelm
Wed Jul 14 13:07:09 1999 +0200 (1999-07-14)
changeset 7005cc778d613217
parent 7004 c799d0859638
child 7006 46048223e0f9
tuned comments;
src/HOL/Isar_examples/BasicLogic.thy
src/HOL/Isar_examples/Group.thy
src/HOL/Isar_examples/README.html
     1.1 --- a/src/HOL/Isar_examples/BasicLogic.thy	Wed Jul 14 13:06:08 1999 +0200
     1.2 +++ b/src/HOL/Isar_examples/BasicLogic.thy	Wed Jul 14 13:07:09 1999 +0200
     1.3 @@ -27,7 +27,7 @@
     1.4  qed;
     1.5  
     1.6  lemma K': "A --> B --> A";
     1.7 -proof single+; txt {* better use sufficient-to-show here \dots *};
     1.8 +proof single+   -- {* better use sufficient-to-show here \dots *};
     1.9    assume A;
    1.10    show A; .;
    1.11  qed;
     2.1 --- a/src/HOL/Isar_examples/Group.thy	Wed Jul 14 13:06:08 1999 +0200
     2.2 +++ b/src/HOL/Isar_examples/Group.thy	Wed Jul 14 13:07:09 1999 +0200
     2.3 @@ -128,7 +128,7 @@
     2.4    monoid_right_unit:  "x * one = x";
     2.5  
     2.6  text {*
     2.7 - Groups are *not* yet monoids directly from the definition .  For
     2.8 + Groups are *not* yet monoids directly from the definition.  For
     2.9   monoids, right_unit had to be included as an axiom, but for groups
    2.10   both right_unit and right_inverse are derivable from the other
    2.11   axioms.  With group_right_unit derived as a theorem of group theory
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/HOL/Isar_examples/README.html	Wed Jul 14 13:07:09 1999 +0200
     3.3 @@ -0,0 +1,23 @@
     3.4 +<!-- $Id$ -->
     3.5 +<html>
     3.6 +
     3.7 +<head>
     3.8 +<title>HOL/Isar_examples</title>
     3.9 +</head>
    3.10 +
    3.11 +<body>
    3.12 +<h1>HOL/Isar_examples</h1>
    3.13 +
    3.14 +Isar offers a new high-level proof (and theory) language interface to
    3.15 +Isabelle.  This directory contains some example Isar documents.  See
    3.16 +the <a href="http://isabelle.in.tum.de/Isar/">Isabelle/Isar page</a>
    3.17 +for more information.
    3.18 +
    3.19 +<p>
    3.20 +
    3.21 +Note that the theory files are basically the plain ASCII sources of
    3.22 +what is meant to be actual typeset documents.  Automatic LaTeX / PDF
    3.23 +pretty printing is not yet available.
    3.24 +
    3.25 +<body>
    3.26 +</html>