From 8ab73b1e463ab61fcdea590db2f60786ee96f47e Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Tue, 16 Jul 2002 17:49:45 +0000
Subject: Add { and } example

---
 etc/isar/Parsing.thy | 13 +++++++++++++
 1 file changed, 13 insertions(+)

diff --git a/etc/isar/Parsing.thy b/etc/isar/Parsing.thy
index 2252d96c..68e2864f 100644
--- a/etc/isar/Parsing.thy
+++ b/etc/isar/Parsing.thy
@@ -40,6 +40,19 @@ proof
     qed
 qed
 
+(* Another thing: nesting with { and } can be tricky. *)
+
+theorem and_comms_again: "A & B --> B & A"
+proof
+  assume "A & B" 
+    thus "B & A"
+    proof {
+      assume A B
+	show ?thesis
+	..
+    } qed
+qed
+
 (* Now the end of file is coming up.  Funny things happen
    because PG only knows how commands start, not how they end.
 *)
-- 
cgit v1.2.3