[isabelle-dev] push request (Sublist.thy)

[Tobias Nipkow]

I'll look at it, thanks.

Tobias

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).
> 
> cheers
> 
> chris
> 
> 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).
>>
>> cheers
>>
>> chris
>>
>> 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
>> hgbundle?
>>
>>
>> _______________________________________________
>> isabelle-dev mailing list
>> isabelle-dev at in.tum.de
>> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>>
> 
> 
> This body part will be downloaded on demand.
>