Julin Shaji (Feb 12 2025 at 05:01): Julin Shaji (Feb 12 2025 at 05:01):Is notepad begin ... end used for temporary things in isabelle?
How are they meant to be used?
Is there some place where we can read about it?
Julin Shaji (Feb 12 2025 at 05:02):Saw this: ' Isar proof body serves as mathematical notepad' at https://isabelle.in.tum.de/doc/isar-ref.pdf
Mathias Fleury (Feb 12 2025 at 05:30):notepad opens a proof context except that you can do whatever you want with assume, fix, ...
Mathias Fleury (Feb 12 2025 at 05:32):It is useful in two cases, showing example:
- in documentation
- in forums (like here or stackoverflow)
It is not really meant to be used in your own development
Manuel Eberl (Mar 02 2025 at 08:13):I use it all the time whenever I don't yet know precisely what the assumptions and conclusions of my theorem will be.
John Hughes (Mar 02 2025 at 15:05):Thank you for asking this, Julin. I, too, was baffled by the reference manual's brief discussion of this.
Last updated: Mar 09 2025 at 12:28 UTC