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.

Larry Paulson


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