Commit 2024-08-08 13:48 a180e024

chore: removing unused Mathport files (#15189) This does not yet remove Mathport.Syntax. We may want to preserve the information about unported tactics implicitly stored there (although this information is quite messy, in large part out of date, and in any case preserved in the git history if anyone wants to do the archaeology).