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

[Dmitriy Traytel]

The test run was ok, but the repository is corrupted once again. Trying 
to repair by stripping.

Dmitriy

On 13.12.2012 13:23, Dmitriy Traytel wrote:
> 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 
>>
>
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev 
>