@Hanna Lachnitt @Yijun He What about a theory Basics.thy to collect very basic things like
set_fourand so on which are duplicated across various files in the library ?
Of course, it's useful only if the attribute
[simp] still works properly.
I factored out various very basic results into a single theory named
Basicswith a rough classification of these results. Thanks to that I cleaned the other theories (no modification was needed, the attributes
[simp] work just fine, I only removed the trivial results). There is no duplication anymore.
So, in the future please use this theory.
When starting a new theory, I advice to import Basics so that Sledgehammer can search it and use the very basic results proved therein.
Last updated: Dec 07 2023 at 16:21 UTC