diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2009-08-17 16:45:41 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2009-08-17 16:45:41 +0000 |
| commit | c8cd8ace98d6e0f3ebdce7718d92229f0c31dbec (patch) | |
| tree | 2afdc999c3e9441ec47e9957d358e4153458f59d /isar/Example.thy | |
| parent | 6c0ea2f4c2fa6c7e4c157080c763902134f5e273 (diff) | |
Move proof-interrupt-process to proof-shell. Add pending interrupt behaviour. See http://proofgeneral.inf.ed.ac.uk/trac/ticket/179
Diffstat (limited to 'isar/Example.thy')
| -rw-r--r-- | isar/Example.thy | 23 |
1 files changed, 21 insertions, 2 deletions
diff --git a/isar/Example.thy b/isar/Example.thy index e869364b..16114823 100644 --- a/isar/Example.thy +++ b/isar/Example.thy @@ -18,7 +18,26 @@ proof qed qed -text {* Proper proof text -- \textit{advanced version}. *} +(* 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 @@ -30,7 +49,7 @@ qed text {* Unstructured proof script. *} -theorem "A & B --> B & A" +theorem "A & B --> B & A" -- {* foo bar *} apply (rule impI) apply (erule conjE) apply (rule conjI) |