[isabelle-dev] Relations vs. Predicates

Lukas Bulwahn bulwahn at in.tum.de
Wed Apr 4 12:30:52 CEST 2012

Hi Chris,

I have tested your changeset on the testboard, and a couple of AFP 
theories break, cf. 
(Some errors are due to your changes, some are due to current work of 
It might be good to provide some patches for the AFP to have a smooth 


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-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20120404/e6a0edb8/attachment-0002.html>

More information about the isabelle-dev mailing list