I'll look at it, thanks. Tobias
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
