Add { and } example

1 files changed, 13 insertions, 0 deletions

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.
 *)