From: Christian Sternagel <c-sterna@jaist.ac.jp>
Dear all,
I recently updated my wqo entry which now also contains a formalization
of Kruskal's tree theorem.
http://afp.sourceforge.net/devel-entries/Well_Quasi_Orders.shtml
Note that this update is currently only available in the development
version (until the next release).
cheers
chris
Last updated: Feb 01 2025 at 20:19 UTC