Commit 2025-06-27 13:04 18d4bf63

feat: Interactive Library Rewrite (#11768) This PR defines the rw?? library rewrite tactic that uses my RefinedDiscrTree. This is a point&click tactic, letting the user click on subexpressions in the main goal. The results are sorted by relevance, and are separated into sections based on the matched pattern. It comes with a filter button that allows you to switch between the (default) filtered view, with removed duplicate lemmas and not showing lemma names, and the complete view. There is also a section for definitionally unfolding the selected expression - these rewrites do not correspond to a library lemma.