Re: [isabelle-dev] HOL/ex/Set_Algebras

2012-04-13 Thread Clemens Ballarin
I wondered when somebody would ask this. What's going on here is a hack, and I'm not very happy about it. If you follow up the imported theory, you will find some code that provides a clone of the interpretation command (under the same name!) with some added functionality (definitions). T

Re: [isabelle-dev] Relations vs. Predicates

2012-04-13 Thread Makarius
On Fri, 13 Apr 2012, Makarius wrote: On AFP I've also seen a machine default for "fetch" merges. This is the canonical configuration for it: [extensions] hgext.fetch = [defaults] fetch = -m "merged" I won't argue about the exact spelling of the "merged", but it should not be the machin

[isabelle-dev] Community Wiki again

2012-04-13 Thread Makarius
On Fri, 13 Apr 2012, Christian Sternagel wrote: Maybe it would be a good idea (for externals and developers) to have some "recipe" (e.g., at the community wiki) This touches again the question of what the community wiki is, or what is could be. So far I am not a member there, because I don't

Re: [isabelle-dev] Relations vs. Predicates

2012-04-13 Thread Makarius
On Fri, 13 Apr 2012, Christian Sternagel wrote: Moreover, incoming changesets needs to be easy to inspect in a few seconds or minutes. (This is why I always ask to write each log item on a separate line, but still with a delimiter such as ";"). Indeed. I hope my commit messages have at least be

Re: [isabelle-dev] Relations vs. Predicates

2012-04-13 Thread Makarius
On Fri, 13 Apr 2012, Christian Sternagel wrote: I didn't use "hg import" yet. Maybe it would be a good idea (for externals and developers) to have some "recipe" (e.g., at the community wiki) that describes how to merge/import third-party changesets most smoothly into the existing history. hg

Re: [isabelle-dev] Relations vs. Predicates

2012-04-13 Thread Makarius
On Fri, 13 Apr 2012, Christian Sternagel wrote: this is just my default user name (and I didn't setup an hg specific one on my local machine). Is my warmup-phase already over? Otherwise I would change the name to "sternagel" (or something similar). (I guess the old changesets will stick with t

Re: [isabelle-dev] Relations vs. Predicates

2012-04-13 Thread Makarius
On Fri, 13 Apr 2012, Lukas Bulwahn wrote: Since your changes 07f4bf913230 and b75ce48a93ee were a bit too long stuck in the pipeline, you then had a non-trivial merge in e1b761c216ac. It seems that Lukus did not want to redo that via a variant of "rebasing" (e.g. plain "hg import" of individu