author wenzelm Tue, 05 Oct 1999 18:16:41 +0200 changeset 7740 2fbe5ce9845f parent 7739 bfe45b716dfc child 7741 874abb8aa65b
 src/HOL/Isar_examples/BasicLogic.thy file | annotate | diff | comparison | revisions src/HOL/Isar_examples/ExprCompiler.thy file | annotate | diff | comparison | revisions src/HOL/Isar_examples/Group.thy file | annotate | diff | comparison | revisions src/HOL/Isar_examples/Peirce.thy file | annotate | diff | comparison | revisions src/HOL/Isar_examples/README.html file | annotate | diff | comparison | revisions
```--- 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```
```--- 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 *};```
```--- 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 *};
```
```--- 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;```
```--- 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 <a href="http://isabelle.in.tum.de/Isar/">Isabelle/Isar page</a>