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

[Tobias Nipkow]

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.
>