[isabelle-dev] push request (Sublist.thy)
nipkow at in.tum.de
Mon Dec 10 08:28:24 CET 2012
I'll look at it, thanks.
Am 09/12/2012 12:50, schrieb Christian Sternagel:
> I fixed an error that only came up during document preparation (which I should
> have tested previously, sorry).
> On 12/09/2012 02:27 PM, Christian Sternagel wrote:
>> Dear all,
>> I have the following changes in my local patch queue:
>> - In src/HOL/Library/Sublist.thy:
>> renamed "emb" ~> "list_hembeq" and "sub" ~> "sublisteq";
>> slightly changed definition of list_hembeq to make it reflexive
>> independent of the base order;
>> dropped predicate "transp_on"
>> Reasons: the name "emb" was very unspecific (hence the "list_" prefix to
>> make clear that it is on lists, and "h" for "homeomorphic" since there
>> is an important difference between "plain" embedding (which is just the
>> sublist relation) and homeomorphic embedding, where we are allowed to
>> replace elements by smaller elements w.r.t. some base order) and in a
>> later development I will need an irreflexive variant (hence "eq").
>> Furthermore, since the basic use of embedding is as a well-quasi-order
>> and wqos are reflexive it seems natural to have a definition where
>> embedding is reflexive independent of the base order.
>> I will add "transp_on" to Restricted_Predicates from the AFP. At some
>> point I would like to have the definitions of "reflp_on", "transp_on",
>> "irreflp_on", "antisymp_on", ... in the main distribution (but that is
>> an orthogonal issue).
>> Any comments? Any takers (for pushing my changes to the main repo)? I
>> checked the changes against f2241b8d0db5 with 'isabelle build -a' and
>> prepared a changeset for the AFP (which I can push myself).
>> PS: As stated above, currently my changes are in my local patch queue
>> and I attached the corresponding patch file from .hg/patches (which
>> contains a commit message at the top). Should I transform this into an
>> isabelle-dev mailing list
>> isabelle-dev at in.tum.de
> This body part will be downloaded on demand.
More information about the isabelle-dev