[isabelle-dev] NEWS: op <infix> -> (<infix>)
Makarius
makarius at sketis.net
Thu Jan 11 14:10:20 CET 2018
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
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.
Makarius
More information about the isabelle-dev
mailing list