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 >> [email protected] >> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev >> > > > This body part will be downloaded on demand. > _______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
