Re: [isabelle] extending well-founded partial orders to total well-founded orders



Dear Andrei,

finally deadlines are over for the time being and I found your email again ;)

On 01/19/2013 12:22 AM, Andrei Popescu wrote:
My AFP formalization ordinals

http://afp.sourceforge.net/entries/Ordinals_and_Cardinals.shtml

I guess since Isabelle2013 this is now "~~/src/HOL/Cardinals/", right?

(hopefully) provides the necessary ingredients: Initial segments in
Wellorder_Embedding, ordinal sum in theory Constructions_on_Wellorders,
and a transfinite recursion combinator (a small adaptation of the
wellfounded combinator) in theory Wellorder_Relation.

Could you elaborate on the mentioned finite recursion combinator and how it is used?

thanks in advance,

chris







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