On 16/05/2025 13:22, Gerwin Klein via isabelle-dev wrote: > > There is a lot of benefit in recording the true history as we do in Isabelle, > even if that history is less perfect. True history is very important. I would call that more perfect than a history that is manipulated to "look better". Makarius