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

[Dmitriy Traytel]

It worked for me. I'm currently building (or more precisely running the 
build tool ;-) ) and will push if it succeeds.

Dmitriy

On 13.12.2012 12:53, Tobias Nipkow wrote:
> I tried to apply your patch but failed (see below). Since I had a problem with
> somebody else's patch before, I wonder if something is wrong at my end? Any
> suggestions?
>
> Tobias
>
> $ hg import emb
> applying emb
> patching file NEWS
> Hunk #1 FAILED at 172
> Hunk #2 FAILED at 181
> 2 out of 2 hunks FAILED -- saving rejects to file NEWS.rej
> patching file src/HOL/BNF/Examples/TreeFI.thy
> Hunk #1 FAILED at 11
> 1 out of 1 hunks FAILED -- saving rejects to file
> src/HOL/BNF/Examples/TreeFI.thy.rej
> patching file src/HOL/BNF/Examples/TreeFsetI.thy
> Hunk #1 FAILED at 11
> 1 out of 1 hunks FAILED -- saving rejects to file
> src/HOL/BNF/Examples/TreeFsetI.thy.rej
> patching file src/HOL/Library/Sublist.thy
> Hunk #1 FAILED at 2
> Hunk #2 FAILED at 10
> Hunk #3 FAILED at 22
> Hunk #4 FAILED at 30
> Hunk #5 FAILED at 42
> Hunk #6 FAILED at 87
> Hunk #7 FAILED at 105
> Hunk #8 FAILED at 190
> Hunk #9 FAILED at 206
> Hunk #10 FAILED at 267
> Hunk #11 FAILED at 419
> 11 out of 11 hunks FAILED -- saving rejects to file src/HOL/Library/Sublist.thy.rej
> patching file src/HOL/Library/Sublist_Order.thy
> Hunk #1 FAILED at 20
> Hunk #2 FAILED at 39
> 2 out of 2 hunks FAILED -- saving rejects to file
> src/HOL/Library/Sublist_Order.thy.rej
> abort: patch failed to apply
>
>
> 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.
>>
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev