On Wed, 17 Oct 2012, Makarius wrote:
Does anybody remember a use of the 'apply_end' command? Many years ago
it was introduced to help analyse the failure of 'qed', in symmetry to
'apply' to break up 'proof' and 'by' steps. That should now work
without it, just by letting 'qed' crash and looking at the error
message. Of course, 'apply' has other uses and is not affected here.
Myself I've almost forgotten about 'apply_end', before constantly
reminded of its existence by the Isabelle/jEdit completion, which
proposes it when the user tries to write 'apply'. So there is a clear
motivation to get rid of the old 'apply_end' feature.
The conclusion of this side-remark is now in Isabelle/599c935aac82:
apply_end stays as before, but there is a way to censor the command
completion table. I am not very fond of censorship, but there is no need
to encumber users by the full complexity of the history of Isar commands
that happens to be still active today.
Users can lead a happy live over several decades without ever getting
exposed to apply_end. And people who happen to know it and use it
occasionally, can easily type in the keyword as a whole.
Makarius
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
