Qiyuan Xu (Jun 15 2021 at 04:05): Qiyuan Xu (Jun 15 2021 at 04:05):How to get all simplification/elimination/introduction/destruction rules (that are marked by the attribute simp, elim, intro and dest) in the current context?
I want something like a group of facts (e.g. ac_simps) that can be used in methods so that I can have methods erule_tac all_elimination_rules and elim all_elimination_rules to apply all elimination rules. Is that possible?
Qiyuan Xu (Jun 15 2021 at 04:42):BTW, is there any way to see what is resulted by elimination rules in the method auto and blast?
Last updated: Nov 13 2025 at 04:27 UTC