From de6ec194f89ccf50b55109957cc6eae9bbec5307 Mon Sep 17 00:00:00 2001
From: Makarius Wenzel
Date: Thu, 27 May 1999 19:27:27 +0000
Subject: be chatty;

---
 isar/Example.thy | 9 +++++++++
 1 file changed, 9 insertions(+)

(limited to 'isar/Example.thy')

diff --git a/isar/Example.thy b/isar/Example.thy
index 8dc4b04a..f9807888 100644
--- a/isar/Example.thy
+++ b/isar/Example.thy
@@ -1,6 +1,10 @@
 
 theory Example = Main:;
 
+text {*
+ Just a few tiny examples to get an idea of how Isabelle/Isar proof documents
+ may look like.
+ *}
 
 lemma I: "A --> A";
 proof;
@@ -17,6 +21,11 @@ proof;
   qed;
 qed;
 
+text {*
+ This one is a good test for ProofGeneral to cope with block-structured
+ proof texts.  Have fun with automatic indentation!
+ *};
+
 lemma S: "(A --> B --> C) --> (A --> B) --> A --> C";
 proof;
   assume "A --> B --> C";
-- 
cgit v1.2.3