Re: [isabelle] [Isabelle2016-1-RC2] Experience with auto-indentation
I agree with Gerwin. The default indentation makes it clear how many subgoals are being solved at each point. Itâs worth knowing that, even if it looks silly.
> On 5 Dec 2016, at 07:54, Gerwin.Klein at data61.csiro.au wrote:
> This is great :-)
> The indentation of auto looks a bit silly but carries information, and should be the way it is.
> This indentation is also what the AFP expects. Weâre not going to argue (much) about this particular case, but itâs usually better to have consistency over beauty in code layout.
This archive was generated by a fusion of
Pipermail (Mailman edition) and