* HOL/Codatatype: New (co)datatype package with support for mixed, nested recursion and interesting non-free datatypes. * HOL/Ordinals_and_Cardinals: Theories of ordinals and cardinals (supersedes the AFP entry of the same name). Kudos to Andrei and Dmitriy! Jasmin