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
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
