@Hanna Lachnitt @Yijun He What about a theory Basics.thy to collect very basic things like set_two
, set_four
and so on which are duplicated across various files in the library ?
Of course, it's useful only if the attribute [simp]
still works properly.
Done!
I factored out various very basic results into a single theory named Basics
with 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: Oct 12 2024 at 20:18 UTC