[isabelle-dev] NEWS: op <infix> -> (<infix>)

[Tobias Nipkow]

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 
that ;-)

Tobias

> 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
> 

-------------- next part --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 5156 bytes
Desc: S/MIME Cryptographic Signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20180111/465a6ce5/attachment.bin>