[isabelle-dev] Relations vs. Predicates
c-sterna at jaist.ac.jp
Wed Apr 4 09:20:26 CEST 2012
On 03/31/2012 01:10 AM, Florian Haftmann wrote:
>> PS: I suggest to rename "rel_comp" into "relcomp" (to be consistent with
> 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.)
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 9534 bytes
Desc: not available
More information about the isabelle-dev