diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2002-07-16 17:49:45 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2002-07-16 17:49:45 +0000 |
| commit | 8ab73b1e463ab61fcdea590db2f60786ee96f47e (patch) | |
| tree | 124859e9ce473bec0df63d0a6a6ad92c0f2f75dd /etc/isar/Parsing.thy | |
| parent | 1674269f9067425f465b90a22c0c316758c8c6a5 (diff) | |
Add { and } example
Diffstat (limited to 'etc/isar/Parsing.thy')
| -rw-r--r-- | etc/isar/Parsing.thy | 13 |
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. *) |