This is just a reminder that the time for non-essential changes to ML and thy sources has already run out last week! There are still a few days to work on the manuals -- without changing the main theory sources of the underlying library, though. Makarius