diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2009-05-26 09:10:38 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2009-05-26 09:10:38 +0000 |
| commit | 89260fcde1b9d0cdd3555d82711fb210ad61fb33 (patch) | |
| tree | 42b3c414727e4c59385f20e7a61d587f2b658e56 /etc/isar | |
| parent | c28a965bd7a90be9f11843ef96549ab8269d43dc (diff) | |
Revise example for Isabelle 2009, showing use of two commands on a line.
Diffstat (limited to 'etc/isar')
| -rw-r--r-- | etc/isar/Sendback.thy | 15 |
1 files changed, 10 insertions, 5 deletions
diff --git a/etc/isar/Sendback.thy b/etc/isar/Sendback.thy index ee68b80a..8bfe8492 100644 --- a/etc/isar/Sendback.thy +++ b/etc/isar/Sendback.thy @@ -6,13 +6,18 @@ theory Sendback imports Main begin ML {* fun sendback cmd = ProofGeneral.sendback "Try this:" [Pretty.str cmd] +fun sendback2 cmd1 cmd2 = + writeln ("Try: " ^ (Markup.markup Markup.sendback cmd1) ^ " or " ^ + (Markup.markup Markup.sendback cmd2)) *} theorem and_comms: "A & B --> B & A" proof - ML {* sendback "assume \"A & B\"" *} - ML {* sendback "then show \"B & A\"" *} - ML {* sendback "proof assume B and A then" *} - ML {* sendback "show ?thesis .. qed" *} - ML {* sendback "qed" *} + ML_command {* sendback "assume \"A & B\"" *} + ML_command {* sendback "show \"B & A\"" *} + ML_command {* sendback2 "proof assume B and A then" + "proof assume A and B then" *} + ML_command {* sendback "show ?thesis .. qed" *} + ML_command {* sendback "qed" *} +qed qed |