be chatty;

1 files changed, 9 insertions, 0 deletions

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";