diff options
Diffstat (limited to 'isar/Example.thy')
-rw-r--r-- | isar/Example.thy | 18 |
1 files changed, 14 insertions, 4 deletions
diff --git a/isar/Example.thy b/isar/Example.thy index 179b5b83..357fa09e 100644 --- a/isar/Example.thy +++ b/isar/Example.thy @@ -11,20 +11,30 @@ theory Example = Main: -text {* Proper proof text. *} +text {* Proper proof text -- naive version. *} theorem and_comms: "A & B --> B & A" proof assume "A & B" - thus "B & A" + then show "B & A" proof assume B and A - thus ?thesis .. + then show ?thesis .. qed qed -text {* Proof script. *} +text {* Proper proof text -- advanced version. *} + +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" apply (rule impI) |