Email Gateway (Oct 25 2025 at 11:49): Email Gateway (Oct 25 2025 at 11:49):From: Lawrence Paulson <lp15@cam.ac.uk>
I am happy to announce this new contribution, by Manuel Eberl, which formalises concepts to ease manipulation of paths e.g. for complex analysis. It also provides the path tactic, which proves or simplifies some common proof obligations for composite paths, e.g. showing that a path is not self-intersecting or decomposing integrals on a composite path into the integrals on the constituent paths.
https://www.isa-afp.org/entries/Path_Automation.html
Larry Paulson
Last updated: Nov 09 2025 at 20:21 UTC