On 08/10/2021 10:40, Gerwin Klein wrote:
>
>>> Further, a whole lot of constants have been moved around. Why? What does
>>> this improve? This can cause major amounts of renaming work for no gain to
>>> anyone.
>
> Maybe the impression of robustness comes from the incremental way we update
> the AFP. Each specific renaming is obvious to the author of that change and
> likely not hard to automate. On the other hand, being confronted with all of
> these at the same time, and having to find all instances by proof failure is
> time consuming and can be extremely frustrating when you have to hunt in hg
> history for what something has been renamed to.
Side-remark: About 50% of the time I do look at the hg history (using e.g. "hg
grep --all") to see how names evolve, and what needs to be done. This also
applies to magic (simp add: ...) or (simp del: ...) details.
Makarius
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
