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: Nov 21 2024 at 12:39 UTC