diff options
author | Makarius Wenzel <makarius@sketis.net> | 2001-12-27 15:56:52 +0000 |
---|---|---|
committer | Makarius Wenzel <makarius@sketis.net> | 2001-12-27 15:56:52 +0000 |
commit | 102c8aea283a732e17dfd557f2b93cec045ec413 (patch) | |
tree | d4986fa2758cb91f6153af7a25775070bce23b97 /isar/Example.thy | |
parent | de5082468d456bb7f30d628f5268e98628ebeb7e (diff) |
tuned;
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) |