Re: [isabelle] extending well-founded partial orders to total well-founded orders
- To: Andrei Popescu <uuomul at yahoo.com>
- Subject: Re: [isabelle] extending well-founded partial orders to total well-founded orders
- From: Christian Sternagel <c.sternagel at gmail.com>
- Date: Mon, 18 Feb 2013 15:32:27 +0900
- Cc: cl-isabelle-users at lists.cam.ac.uk
- In-reply-to: <1358522523.56111.YahooMailClassic@web120604.mail.ne1.yahoo.com>
- References: <1358522523.56111.YahooMailClassic@web120604.mail.ne1.yahoo.com>
- User-agent: Mozilla/5.0 (X11; Linux x86_64; rv:17.0) Gecko/20130110 Thunderbird/17.0.2
finally deadlines are over for the time being and I found your email
On 01/19/2013 12:22 AM, Andrei Popescu wrote:
My AFP formalization ordinals
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,
This archive was generated by a fusion of
Pipermail (Mailman edition) and