# HG changeset patch
# User wenzelm
# Date 939140201 -7200
# Node ID 2fbe5ce9845f107e86beb87cbc9e924021b64c97
# Parent bfe45b716dfcba9ccc0e3aa14ea9d8f19acd2d54
tuned comments;
diff -r bfe45b716dfc -r 2fbe5ce9845f src/HOL/Isar_examples/BasicLogic.thy
--- a/src/HOL/Isar_examples/BasicLogic.thy Tue Oct 05 18:16:26 1999 +0200
+++ b/src/HOL/Isar_examples/BasicLogic.thy Tue Oct 05 18:16:41 1999 +0200
@@ -8,6 +8,8 @@
theory BasicLogic = Main:;
+subsection {* Some trivialities *};
+
text {* Just a few toy examples to get an idea of how Isabelle/Isar
proof documents may look like. *};
@@ -103,9 +105,9 @@
qed;
-section {* Examples from 'Introduction to Isabelle' *};
+subsection {* A few examples from ``Introduction to Isabelle'' *};
-text {* 'Propositional proof' *};
+subsubsection {* Propositional proof *};
lemma "P | P --> P";
proof;
@@ -125,7 +127,7 @@
qed;
-text {* 'Quantifier proof' *};
+subsubsection {* Quantifier proof *};
lemma "(EX x. P(f(x))) --> (EX x. P(x))";
proof;
@@ -153,7 +155,7 @@
by blast;
-subsection {* 'Deriving rules in Isabelle' *};
+subsubsection {* Deriving rules in Isabelle *};
text {* We derive the conjunction elimination rule from the
projections. The proof below follows the basic reasoning of the
diff -r bfe45b716dfc -r 2fbe5ce9845f src/HOL/Isar_examples/ExprCompiler.thy
--- a/src/HOL/Isar_examples/ExprCompiler.thy Tue Oct 05 18:16:26 1999 +0200
+++ b/src/HOL/Isar_examples/ExprCompiler.thy Tue Oct 05 18:16:41 1999 +0200
@@ -7,7 +7,7 @@
theory ExprCompiler = Main:;
-title {* Correctness of a simple expression/stack-machine compiler *};
+chapter {* Correctness of a simple expression/stack-machine compiler *};
section {* Basics *};
diff -r bfe45b716dfc -r 2fbe5ce9845f src/HOL/Isar_examples/Group.thy
--- a/src/HOL/Isar_examples/Group.thy Tue Oct 05 18:16:26 1999 +0200
+++ b/src/HOL/Isar_examples/Group.thy Tue Oct 05 18:16:41 1999 +0200
@@ -5,7 +5,7 @@
theory Group = Main:;
-title {* Basic group theory *};
+chapter {* Basic group theory *};
section {* Groups *};
diff -r bfe45b716dfc -r 2fbe5ce9845f src/HOL/Isar_examples/Peirce.thy
--- a/src/HOL/Isar_examples/Peirce.thy Tue Oct 05 18:16:26 1999 +0200
+++ b/src/HOL/Isar_examples/Peirce.thy Tue Oct 05 18:16:41 1999 +0200
@@ -5,7 +5,7 @@
theory Peirce = Main:;
-text {* Peirce's law: examples of classical proof. *};
+section {* Examples of classical proof --- Peirce's law. *};
theorem "((A --> B) --> A) --> A";
proof;
diff -r bfe45b716dfc -r 2fbe5ce9845f src/HOL/Isar_examples/README.html
--- a/src/HOL/Isar_examples/README.html Tue Oct 05 18:16:26 1999 +0200
+++ b/src/HOL/Isar_examples/README.html Tue Oct 05 18:16:41 1999 +0200
@@ -13,11 +13,5 @@
the Isabelle/Isar page
for more information.
-
-
-Note that the theory files are basically just plain ASCII sources of
-what are meant to be actual typeset documents. Automatic LaTeX / PDF
-pretty printing will be available in the near future.
-