[isabelle-dev] NEWS: op <infix> -> (<infix>)
nipkow at in.tum.de
Thu Jan 11 18:06:41 CET 2018
On 11/01/2018 14:10, Makarius wrote:
> On 10/01/18 21:46, Tobias Nipkow wrote:
>> I seem to remember Lamport makes a
>> similar point but it is not in his "How to write a proof".]
> The paper is called "How to Write a Long Formula" and available e.g.
> here: https://lamport.azurewebsites.net/pubs/lamport-howtowrite.ps.Z
I think that is the one I meant. Don't worry, I am not suggesting we do it like
> In the early Isar years I have actually studied both "How to write ..."
> papers with some interest, but ended up ignoring most of the ideas.
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 5156 bytes
Desc: S/MIME Cryptographic Signature
More information about the isabelle-dev