[isabelle-dev] Relations vs. Predicates

[Christian Sternagel]

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
-------------- next part --------------
A non-text attachment was scrubbed...
Name: relcompp.hgbundle
Type: application/octet-stream
Size: 9534 bytes
Desc: not available
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20120404/299af3e5/attachment-0002.obj>