[isabelle-dev] Quotient.invariant

[Makarius]

On Sat, 24 Mar 2012, Ondřej Kunčar wrote:

> The constant is now hidden.

Just two more things:

   * "Now" means Isabelle/e64ffc96a49f -- The issue of proper references to 
changesets is a running gag on isabelle-dev already. If you want, you can 
make it the discriminating aspect between the two mailing lists: 
isabelle-dev = proper hg ids, isabelle-users = some official release 
(implicit). This does have a real practical impact, because old mail 
threads are often studied later, e.g. 2 weeks or 2 months or 2 years.  For 
official releases the date stamp is sufficient, for continuous development 
proper ids are required.

   * The log entry for e64ffc96a49f is merely a rewording of the diff in 
English prose, i.e. empty.  There is an art of writing in half a sentence 
what was done and why, to a give a hint to the one who needs to understand 
things later (often many years).  There is also a realistic danger of 
fluctuation of small mishaps back and forth, if the history does not 
explain the reasons.


 	Makarius