diff options
| -rw-r--r-- | etc/isar/Sendback.thy | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/etc/isar/Sendback.thy b/etc/isar/Sendback.thy index 5d0ac019..ee68b80a 100644 --- a/etc/isar/Sendback.thy +++ b/etc/isar/Sendback.thy @@ -11,8 +11,8 @@ fun sendback cmd = ProofGeneral.sendback "Try this:" [Pretty.str cmd] 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 "then show \"B & A\"" *} + ML {* sendback "proof assume B and A then" *} + ML {* sendback "show ?thesis .. qed" *} ML {* sendback "qed" *} qed |