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

Peter Lammich lammich at in.tum.de
Tue Jan 16 19:12:18 CET 2018


On Di, 2018-01-16 at 16:31 +0000, Lawrence Paulson wrote:
> I know how to do it, but no beginner could ever find this.
> Larry
This is usually one of the first things I show students learning
Isabelle ... I'm using brackets syntax in demos, but let 
them decide which syntax they like better.
Peter
> 

> > On 16 Jan 2018, at 16:20, Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch> wrote:

> > It's not too hard: Go to Plugins/Plugin Options/Isabelle/General and enter "brackets" under Print mode.

> _______________________________________________
> isabelle-dev mailing list
> 
isabelle-dev at in.tum.de> 
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev> 
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20180116/c7ba227b/attachment-0002.html>


More information about the isabelle-dev mailing list