diff options
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 |