Re: [isabelle] how to set "brackets" mode

Different people have different preferences, of course.  For me, it is precisely the nesting that makes a clearly bracketed notation preferable. A flat list like [a,b,c,d,e,f,g] is no less readable if written as a::b::c::d::e::f::g::nil. But consider [a,[b,c],[d,e],[f,g]].

Also, with large formulas, it isnât always clear whether â ==> A is the conclusion or just another premise.


> On 20 Dec 2016, at 18:31, Makarius <makarius at> wrote:
> The uniform notation of nested ==> goes back to 1998, when Isar concepts
> were emerging, with some consequences on Pure. E.g. it became possible
> to work with nested rules routinely. Before, rules were mostly flat and
> the bracketed notation was adequate. Afterwards, I found nested rules
> with brackets very cumbersome to read and to write, and eventually
> stopped doing that. 

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.