[isabelle] New to the AFP: Countable Ordinals

Many thanks to Brian Huffman for his recent contribution to the Archive of Formal Proofs (abstract attached).

See http://afp.sourceforge.net/entries/Ordinal.shtml

Larry Paulson

Countable Ordinals

This development defines a well-ordered type of countable ordinals.
It includes notions of continuous and normal functions, recursively
defined functions over ordinals, least fixed-points, and derivatives.
Much of ordinal arithmetic is formalized, including exponentials and
logarithms. The development concludes with formalizations of Cantor
Normal Form and Veblen hierarchies over normal functions.

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.