Re: [isabelle-dev] Relations vs. Predicates
Here is another follow-up to the relcomp story so far: changeset: 47508:85c6268b4071 tag: tip user:wenzelm date:Tue Apr 17 16:48:37 2012 +0200 files: doc-src/TutorialI/Sets/Relations.thy description: updated rel_comp ~ relcomp (cf. e1b761c216ac); doc-src/TutorialI/Sets/Relations.thy This is only to make the manual compile again. I hope it is not one of the theories that need generated latex copied to another place by hand. Moreover NEWS in that version has oddities like this: rel_comp_def ~ rel_comp_unfold and later rel_comp_unfold ~ relcomp_unfold In the time immediately before the relase (which is now) the NEWS should reflect the perspective for end-users of the official stable system that is delivered. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Relations vs. Predicates
Sorry for the inconveniences. On 04/17/2012 11:55 PM, Makarius wrote: Here is another follow-up to the relcomp story so far: changeset: 47508:85c6268b4071 tag: tip user: wenzelm date: Tue Apr 17 16:48:37 2012 +0200 files: doc-src/TutorialI/Sets/Relations.thy description: updated rel_comp ~ relcomp (cf. e1b761c216ac); doc-src/TutorialI/Sets/Relations.thy This is only to make the manual compile again. This one didn't show up during 'isabelle makeall all'. Shouldn't documentation be part of all? I guess then that a test should also include ./Admin/build doc? Anything else besides isabelle makeall all ./Admin/build doc to test a changeset (apart from external dependencies like the AFP)? I hope it is not one of the theories that need generated latex copied to another place by hand. Just out of curiosity: what do you mean by the above statement? Moreover NEWS in that version has oddities like this: rel_comp_def ~ rel_comp_unfold and later rel_comp_unfold ~ relcomp_unfold In the time immediately before the relase (which is now) the NEWS should reflect the perspective for end-users of the official stable system that is delivered. I observed this oddities but left them deliberately since I was not aware of the above convention (which is of course very sensible). cheers chris ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Relations vs. Predicates
On 04/16/2012 09:13 AM, Christian Sternagel wrote: Hi all, On 04/03/2012 02:51 AM, Florian Haftmann wrote: well, I suggest to augment the existing theory with lemmas transferred from relpow to relpowp to emphasize that both worlds exists and that lemmas can be found easier by find_theorems. The typical pattern is lemma foo_relpow: ... proof lemma foo_relpowp: ... by (fact foo_relpow [to_pred]) I did this in the meantime (tested with isabelle makeall all). This time as a patch (in order to avoid cluttering the history) on Theory Transitive_Closure. Suggested NEWS entry: -- * Theory Transitive_Closure: Duplicated facts about relpow for relpowp to emphasize that both worlds exist and facilitate better results with find_theorems. Added Lemmas: relpowp_1 relpowp_0_I relpowp_Suc_I relpowp_Suc_I2 relpowp_0_E relpowp_Suc_E relpowp_E relpowp_Suc_D2 relpowp_Suc_E2 relpowp_Suc_D2' relpowp_E2 relpowp_add relpowp_commute relpowp_bot rtranclp_imp_Sup_relpowp relpowp_imp_rtranclp rtranclp_is_Sup_relpowp rtranclp_power tranclp_power rtranclp_imp_relpowp relpowp_fun_conv -- I pushed your changes to the public repository, but I did not consider the NEWS entry worth mentioning -- we add theorems on a daily basis, without explicitly advertising them in the NEWS. Lukas cheers chris ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Relations vs. Predicates
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 individual changesets on tip), so he re-merged the whole thing with his current tip in d8fad618a67a and then pushed it. I tried to do the rebase, but as the merge was non-trivial, the rebasing would have taken again quite some time, so I risked having a long edge in the repository graph instead. Which means I've read the history correctly. It was OK in that situation, especially since griff is still warming up. I guess for the future, especially external contributions should provide patches without merges, but instead make sure that the patches can be applied to the current tip (even though this requires some maintenance from the contributor while internals are reviewing the changeset). Basically we already have the principle that contributions form a single chain of changes wrt. a recent tip of the repository, without any merge attempts yet. Such a branch should normally graft easily on the latest local tip (without rebasing), if it is not too old yet. Since external contributions happen so rarely, the process is hardly routine. So it needs some more practice to make it work smoothly both for contributors and maintainers pushing. I think that recent Mercurial now has a stable rebase command, so one should probably look there as well. Personally, I do not like heavy rewriting of history, as is done routinely on many git projects -- it can introduce mistakes that are not recorded anywhere, while a messy merge at least contains the information in principle. A little bit of rebasing of 1 or 2 weeks time gap might work out smoothly, nonetheless. BTW, since a year or so I try to make small contributions to jEdit, but I am still not there yet. They have a rather awkward process that I do not quite understand, so whatever I do for jEdit is syntactically incorrect and ill-typed. At least I've managed to excite some jEdit experts for the \A Unicode problem. Another one even started looking into proper right-to-left type-setting, say for Arabic, but it is not going to happen soon. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Relations vs. Predicates
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 been correct in this respect? I've mentioned the line separation specifically for Isabelle/b75ce48a93ee. The README_REPOSITORY has this long exposition on this detail: * The standard changelog entry format of the Isabelle repository admits several (vaguely related) items to be rolled into one changeset. Each item is then described on a separate line that may become longer as screen line and is terminated by punctuation. These lines are roughly ordered by importance. This format conforms to established Isabelle tradition. In contrast, the default of Mercurial prefers a single headline followed by a long body text. The reason for that is a somewhat different development model of typical distributed projects, where external changes pass through a hierarchy of reviewers and maintainers, until they end up in some authoritative repository. Isabelle changesets can be more spontaneous, growing from the bottom-up. The web style of http://isabelle.in.tum.de/repos/isabelle/ accommodates the Isabelle changelog format. Note that multiple lines will sometimes display as a single paragraph in HTML, so some terminating punctuation is required. Do not squeeze multiple items on the same line in the original text! It takes a few extra seconds in the routine eye balling process to reparse a long line to chop it into the respective items. This time is better invested in looking at the content. I hope that I am not the only one who keeps an eye on incoming changes; there are often small issues that need to be discussed. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Relations vs. Predicates
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 machine generated thing. Here is another one just coming in: changeset: 47453:598604c91036 tag: tip parent: 47449:5e1482296b12 parent: 47452:60da1ee5363f user:Andreas Lochbihler date:Fri Apr 13 13:30:27 2012 +0200 summary: Automated merge with ssh://macbroy25.informatik.tu-muenchen.de//home/isabelle-repository/repos/isabelle Again, the digested content of README_REPOSITORY is important. There are deeper things in there, but at least the superficial things should be done right as a start. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Relations vs. Predicates
On Wed, 11 Apr 2012, Christian Sternagel wrote: On 04/05/2012 12:30 PM, Christian Sternagel wrote: Hi Lukas, thanks for testing! (Sorry for the late reply, currently my internet-connectivity is rather sporadic ;)). Please find attached a hg bundle that does the name change 'rel_comp - relcomp' for the AFP. It seems that Lukas has now pushed that, see Isabelle/d8fad618a67a I now also know who this mysterious griff from AFP is :-) Seriously, you have the free choice to specify your user name for Isabelle hg contributions, but you need to stick to it in the long run. In the initial warmup-phase you have one chance to rethink the initial choice, but do not have to do so. Is something wrong with my changesets? ;) You are an experienced Mercurial user already, so there are few technical things to say here. Semantically, the principles in the (slightly long) file README_REPOSITORY of the Isabelle repository apply, even when things are pushed by an intermediary person with administrative push access (the latter is also resposible to inspect incoming things in this respect). In the explanations there is a section about merges with a few important hints: * Accumulate private commits for a maximum of 1-3 days. ... * Test the merged result as usual and push back in real time. Piling private changes and public merges longer than 0.5-2 hours is apt to produce some mess when pushing eventually! 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 individual changesets on tip), so he re-merged the whole thing with his current tip in d8fad618a67a and then pushed it. Isn't it nice what the history of Mercurial tells? When producing the history one also needs to keep readability and clarity in mind -- it needs to be studied routinely when sorting out problems. 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 ;). Nothing bad happened despite all these static type errors in the above changes, nonetheless one needs to maintain a routine of correctness by construction of Isabelle history. Over the years, I had occasionally spent several hours or days (or rather nights) trying to disentangle unclear situations for particularly odd changesets. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Relations vs. Predicates
Hi Makarius, On 04/13/2012 03:12 AM, Makarius wrote: I now also know who this mysterious griff from AFP is :-) Seriously, you have the free choice to specify your user name for Isabelle hg contributions, but you need to stick to it in the long run. In the initial warmup-phase you have one chance to rethink the initial choice, but do not have to do so. Maybe christ would be better ;). But seriously, 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 the awkward name?) And thanks for the detailed comments. Piling private changes and public merges longer than 0.5-2 hours is apt to produce some mess when pushing eventually! I don't see how this can be avoided when pushing as an external from a different time zone. 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 individual changesets on tip), so he re-merged the whole thing with his current tip in d8fad618a67a and then pushed it. 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. Isn't it nice what the history of Mercurial tells? When producing the history one also needs to keep readability and clarity in mind -- it needs to be studied routinely when sorting out problems. 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 been correct in this respect? Nothing bad happened despite all these static type errors in the above changes, nonetheless one needs to maintain a routine of correctness by construction of Isabelle history. Over the years, I had occasionally spent several hours or days (or rather nights) trying to disentangle unclear situations for particularly odd changesets. Unfortunately there are not so many people who know all this, and Makarius' wisdom only comes by hindsight with fire and brimstone. ;) (Just kidding! I'm glad about any comments that increase my understanding.) - chris (a.k.a. griff ... this almost sounds alike ... if you lisp) PS: sorry for being partly off topic. ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Relations vs. Predicates
Hi all, On 03/31/2012 01:10 AM, Florian Haftmann wrote: PS: I suggest to rename rel_comp into relcomp (to be consistent with relpow). This would also mean to rename the corresponding lemmas, although I would also appreciate consistency. Also the »pred_comp« abbreviation should be dropped, with the subsequent consequences for theorem names. This would also be something you could contribute if you like. The attached hg bundle contains the renaming from rel_comp to relcomp, and replaces all occurances (also in lemma names) of the abbreviation pred_comp by relcompp. I tested the bundle (with isabelle makeall all) against changeset e1b761c216ac. Only HOL-Metis_Examples failed. Could this failure be due to the fact that my machine only uses remote_ versions of ATPs. Or is this really related to my change? (Currently I don't see how.) cheers chris relcompp.hgbundle Description: Binary data ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Relations vs. Predicates
Hi Chris, I have tested your changeset on the testboard, and a couple of AFP theories break, cf. http://isabelle.in.tum.de/testboard/Isabelle/report/edd1df5c8daf4109a6366801aaeff7fd (Some errors are due to your changes, some are due to current work of others.) It might be good to provide some patches for the AFP to have a smooth transition. Lukas On 04/04/2012 09:20 AM, Christian Sternagel wrote: Hi all, On 03/31/2012 01:10 AM, Florian Haftmann wrote: PS: I suggest to rename rel_comp into relcomp (to be consistent with relpow). This would also mean to rename the corresponding lemmas, although I would also appreciate consistency. Also the »pred_comp« abbreviation should be dropped, with the subsequent consequences for theorem names. This would also be something you could contribute if you like. The attached hg bundle contains the renaming from rel_comp to relcomp, and replaces all occurances (also in lemma names) of the abbreviation pred_comp by relcompp. I tested the bundle (with isabelle makeall all) against changeset e1b761c216ac. Only HOL-Metis_Examples failed. Could this failure be due to the fact that my machine only uses remote_ versions of ATPs. Or is this really related to my change? (Currently I don't see how.) cheers chris ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Relations vs. Predicates
Hi Christian, Sorry, I'm not familiar with the developer workflow. I do have a cloned hg repo of Isabelle (from http://isabelle.in.tum.de/repos/isabelle), but I don't see an IsaMakefile (which would be required for isabelle make all). Where is this IsaMakefile located? it is »isabelle makeall all« (sorry, this was my fault). Cheers, Florian -- PGP available: http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Relations vs. Predicates
Hi Christian, this has been added in http://isabelle.in.tum.de/testboard/Isabelle/rev/69cee87927f0 – you can transfer theorems from the set relations in an ad-hoc using [to_pred]. You can also prove theorems for pred relations by means of … by (fact … [to_pred]), as has been done in many places of theory Relation. This could also be a contribution to the Isabelle theories for the next release. I do not fully understand. I see how [to_pred] can be used to transfer results, but what kind of theorems are you referring to? Do you mean to do this for every theorem on relations to have an equivalent for binary predicates? well, I suggest to augment the existing theory with lemmas transferred from relpow to relpowp to emphasize that both worlds exists and that lemmas can be found easier by find_theorems. The typical pattern is lemma foo_relpow: … proof lemma foo_relpowp: … by (fact foo_relpow [to_pred]) I will give it a try. Anyway, how would I commit such a contribution? Sending a patch to the mailing list? And is it enough that ./build -b HOL works or are there any other places I have to consider (e.g., the AFP)? Well, you could check with an check an »isabelle make all«, send the patch to the mailing list, and somebody else would take care for AFP and the remaining technicalities. You could also clone the existing hg http://isabelle.in.tum.de/reports/Isabelle and provide an URL to import your patch from. Or think of whatever workflow hg offers. Cheers, Florian -- PGP available: http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de signature.asc Description: OpenPGP digital signature ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Relations vs. Predicates
Hi Christian, by the way, I noticed that sometimes [to_pred] yields undesirable results (containing case-expressions), e.g., thm trancl_power[to_pred] results in (case ?p of (x, xa) ⇒ ?R^++ x xa) = (∃n0. case ?p of (x, xa) ⇒ (?R ^^ n) x xa) is this an inherent problem or could this be repaired by adding appropriate [pred_set_conv] (I do not know how this workds in detail). I do not know whether this is inherent (Stefan could know). There are (at least) two solutions: * [unfold prod_case_unfold] * [of (a, b), unfold some suitable rule] Note that internally prod_case is also used as »uncurry« combinator. Hope this helps, Florian -- PGP available: http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de signature.asc Description: OpenPGP digital signature ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Relations vs. Predicates
Hi Florian,
On 03/31/2012 01:10 AM, Florian Haftmann wrote:
Hi Christian,
To come back to the subject, I'm missing iteration of predicates,
i.e., what _^^n is on relations but for predicates ('a = 'a =
bool).
this has been added in
http://isabelle.in.tum.de/testboard/Isabelle/rev/69cee87927f0 – you can
transfer theorems from the set relations in an ad-hoc using [to_pred].
You can also prove theorems for pred relations by means of … by (fact …
[to_pred]), as has been done in many places of theory Relation. This
could also be a contribution to the Isabelle theories for the next release.
I do not fully understand. I see how [to_pred] can be used to transfer
results, but what kind of theorems are you referring to? Do you mean to
do this for every theorem on relations to have an equivalent for binary
predicates?
PS: I suggest to rename rel_comp into relcomp (to be consistent with
relpow).
This would also mean to rename the corresponding lemmas, although I
would also appreciate consistency. Also the »pred_comp« abbreviation
should be dropped, with the subsequent consequences for theorem names.
This would also be something you could contribute if you like.
I will give it a try. Anyway, how would I commit such a contribution?
Sending a patch to the mailing list? And is it enough that ./build -b
HOL works or are there any other places I have to consider (e.g., the AFP)?
cheers
chris
In @{theory Relation} there is a typo in the lemma name
prod_comp_bot1.
Fixed, thanks a lot.
Cheers,
Florian
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Relations vs. Predicates
Dear all,
by the way, I noticed that sometimes [to_pred] yields undesirable
results (containing case-expressions), e.g.,
thm trancl_power[to_pred]
results in
(case ?p of (x, xa) ⇒ ?R^++ x xa) =
(∃n0. case ?p of (x, xa) ⇒ (?R ^^ n) x xa)
is this an inherent problem or could this be repaired by adding
appropriate [pred_set_conv] (I do not know how this workds in detail).
cheers
chris
On 03/31/2012 03:00 PM, Christian Sternagel wrote:
Hi Florian,
On 03/31/2012 01:10 AM, Florian Haftmann wrote:
Hi Christian,
To come back to the subject, I'm missing iteration of predicates,
i.e., what _^^n is on relations but for predicates ('a = 'a =
bool).
this has been added in
http://isabelle.in.tum.de/testboard/Isabelle/rev/69cee87927f0 – you can
transfer theorems from the set relations in an ad-hoc using [to_pred].
You can also prove theorems for pred relations by means of … by (fact …
[to_pred]), as has been done in many places of theory Relation. This
could also be a contribution to the Isabelle theories for the next
release.
I do not fully understand. I see how [to_pred] can be used to transfer
results, but what kind of theorems are you referring to? Do you mean to
do this for every theorem on relations to have an equivalent for binary
predicates?
PS: I suggest to rename rel_comp into relcomp (to be consistent with
relpow).
This would also mean to rename the corresponding lemmas, although I
would also appreciate consistency. Also the »pred_comp« abbreviation
should be dropped, with the subsequent consequences for theorem names.
This would also be something you could contribute if you like.
I will give it a try. Anyway, how would I commit such a contribution?
Sending a patch to the mailing list? And is it enough that ./build -b
HOL works or are there any other places I have to consider (e.g., the
AFP)?
cheers
chris
In @{theory Relation} there is a typo in the lemma name
prod_comp_bot1.
Fixed, thanks a lot.
Cheers,
Florian
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Relations vs. Predicates
Hi Christian,
To come back to the subject, I'm missing iteration of predicates,
i.e., what _^^n is on relations but for predicates ('a = 'a =
bool).
this has been added in
http://isabelle.in.tum.de/testboard/Isabelle/rev/69cee87927f0 – you can
transfer theorems from the set relations in an ad-hoc using [to_pred].
You can also prove theorems for pred relations by means of … by (fact …
[to_pred]), as has been done in many places of theory Relation. This
could also be a contribution to the Isabelle theories for the next release.
PS: I suggest to rename rel_comp into relcomp (to be consistent with
relpow).
This would also mean to rename the corresponding lemmas, although I
would also appreciate consistency. Also the »pred_comp« abbreviation
should be dropped, with the subsequent consequences for theorem names.
This would also be something you could contribute if you like.
In @{theory Relation} there is a typo in the lemma name
prod_comp_bot1.
Fixed, thanks a lot.
Cheers,
Florian
--
PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
signature.asc
Description: OpenPGP digital signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] Relations vs. Predicates
Hi all,
currently there are two constants
op ^ :: 'b = nat = 'b
op ^^ :: 'b = nat = 'b
making it a bit difficult for the user to choose the correct one in all
situations. As far as I see op ^^ is just syntax for the overloaded
compow. Shouldn't it be possible to unify this (and also relpow) by
using adhoc overloading, so that only one operator, e.g., op ^ remains?
To come back to the subject, I'm missing iteration of predicates,
i.e., what _^^n is on relations but for predicates ('a = 'a =
bool). (Why are predicates less developed than relations anyway?)
cheers
chris
PS: I suggest to rename rel_comp into relcomp (to be consistent with
relpow). In @{theory Relation} there is a typo in the lemma name
prod_comp_bot1.
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
