Dear Dmitriy,
thanks for pushing! (I hope the repository trouble is not connected to
my changesets ;))
cheers
chris
On 12/13/2012 09:58 PM, Dmitriy Traytel wrote:
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
[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
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
