[isabelle-dev] Relations vs. Predicates

[Lukas Bulwahn]

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-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>