diff options
Diffstat (limited to 'etc')
| -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. *) |