diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2009-08-20 11:00:44 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2009-08-20 11:00:44 +0000 |
| commit | c440ded61788d0718065c494f7f19065da0e7e03 (patch) | |
| tree | 67aa3220786aeb8f3d66b6e15c33a0a05315b598 | |
| parent | b6172fb5ea2541633b5fad8ab6213b3d70aea975 (diff) | |
Remove spurious junk.
| -rw-r--r-- | isar/Example.thy | 31 |
1 files changed, 1 insertions, 30 deletions
diff --git a/isar/Example.thy b/isar/Example.thy index 16114823..34c840fe 100644 --- a/isar/Example.thy +++ b/isar/Example.thy @@ -18,38 +18,9 @@ proof qed qed -(* but on the other hand, who knows? *) - -text {* Proper proof text -- \textit{advanced ve"rs"ion}. What do you think? Who knows. *} -theorem "B & A --> A & B" -proof - assume "B & A" -- "one of those kinds" - then obtain A and B .. - then show "A & B" .. -qed - - -(* foo bar wiggle *) - -theorem "A & B --> B & A" -proof - assume "A & B" - then obtain B and A .. - then show "B & A" .. -qed - - -theorem "A & B --> B & A" -proof - assume "A & B" - then obtain B and A .. - then show "B & A" .. -qed - - text {* Unstructured proof script. *} -theorem "A & B --> B & A" -- {* foo bar *} +theorem "A & B --> B & A" apply (rule impI) apply (erule conjE) apply (rule conjI) |