[isabelle-dev] Word Libraries

[Makarius]

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