Re: [isabelle] Isabelle style guide

> On 28.05.2015, at 22:21, Makarius <makarius at> wrote:
> On Sat, 23 May 2015, Gerwin Klein wrote:
>> Updating lots of proofs to Isabelle2015-RCx and discussions about submission rules for the AFP inspired me to write up guidelines that may be of more widespread use and interest:
> This is indeed a quite fitting style guide.  The Prover IDE should gradually formalize more of such fine points, to make it easier to avoid bad style by default.

I agree, it would be nice to gradually converge to more support for such things over time.

> * Concerning bad internal names like xa, xb, xaa: Isabelle2015 produces
>  formal markup for that in the slightly reformed rule_tac family, with
>  the faint read color scheme of improper material.  Maybe we should also
>  revisit rename_tac at some point, to clarify its meaning in that
>  respect, or to eliminate the need for rename_tac / rule_tac altogether
>  due to newly emerging subgoal focus in Isar "scriptsâ.

The subgoal focus mechanism sounds promising. I didnât have enough practical experience with it yet to make it a recommendation, but when it has withstood the test of time for a while, that could indeed become the main way of doing things.

> I am curious to see part 2, and especially part 3 about layout; the latter category is more easily accessible in the Prover IDE.

Part 3 will probably be the most controversial one - not because Iâm planning to write anything special, but because layout is the easiest to have strong opinions on.



The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.

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