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