Re: [isabelle] Isabelle style guide
> On 28.05.2015, at 22:21, Makarius <makarius at sketis.net> 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