diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2008-01-31 19:26:13 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2008-01-31 19:26:13 +0000 |
| commit | b9f40e7b69a7df1751ad132179b4bc28e30b43a5 (patch) | |
| tree | a005f698bd5c87d298ab3f8b7acbdf5625ef9b62 /etc | |
| 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).
Diffstat (limited to 'etc')
| -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 |