[isabelle-dev] Relations vs. Predicates

[Christian Sternagel]

Is something wrong with my changesets? ;) - chris

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