[isabelle-dev] informative changelogs / typedef (open) unit

[Makarius]

Hi Brian,

can you say a few words about b994d855dbd2 just for the historical record?

Such changes deep down in HOL easily cause odd problems later on, so the 
one doing the bisection in some years might need more info via the mail 
archive.


I would also like to take the opportunity to recall our most basic 
changelog conventions:

   each item on a separate line;
   items ordered roughly by importance;

For some reason, many people have started to sequeze everything in a 
single line (frequent), or imitate the headline/body text format of other 
projects with a completely different structure (rare).  The reason might 
be as profane as the default web style of Mercurial, but at least on 
http://isabelle.in.tum.de/repos/isabelle the display follows the usual 
Isabelle format.

I spend a good portion of my time inspecting changesets, not just the 
incoming ones, but also really old ones when sorting out problems. So the 
little extra care when composing changelogs will help a lot in the overall 
process.

The recent crash of find_theorems due to b654fa27fbc4 is just one example 
that changes deep in the system need routine reviewing.  It's on my list 
for several weeks, but I did not find the time to look at it so far.


 	Makarius