diff options
| author | David Aspinall | 2008-01-31 19:26:13 +0000 |
|---|---|---|
| committer | David Aspinall | 2008-01-31 19:26:13 +0000 |
| commit | b9f40e7b69a7df1751ad132179b4bc28e30b43a5 (patch) | |
| tree | a005f698bd5c87d298ab3f8b7acbdf5625ef9b62 | |
| parent | b8e119d6a7be4e27aad70817ae1b082f74861bc0 (diff) | |
Remove semi-colons. Literal commands triggered in response buffer
are now sent individually. Should be compatible with original PBP
behaviour which worked from goals buffer (and is anyway no longer used).
| -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 |