Anthony Bordg (Jul 04 2019 at 12:05): Anthony Bordg (Jul 04 2019 at 12:05):@Hanna Lachnitt @Yijun He What about a theory Basics.thy to collect very basic things like set_two, 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.
Anthony Bordg (Jul 04 2019 at 22:08):Done!
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.
Anthony Bordg (Oct 14 2019 at 12:05):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: Nov 02 2025 at 20:20 UTC