[isabelle-dev] Relations vs. Predicates

Christian Sternagel c-sterna at jaist.ac.jp
Thu Apr 5 05:30:14 CEST 2012

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.



On 04/04/2012 07:30 PM, Lukas Bulwahn wrote:
> 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 --------------
A non-text attachment was scrubbed...
Name: relcomp-afp.hgbundle
Type: application/octet-stream
Size: 2190 bytes
Desc: not available
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20120405/15263735/attachment-0002.obj>

More information about the isabelle-dev mailing list