<html>
<head>
<meta content="text/html; charset=ISO-8859-1"
http-equiv="Content-Type">
</head>
<body bgcolor="#FFFFFF" text="#000000">
Hi Chris,<br>
<br>
I have tested your changeset on the testboard, and a couple of AFP
theories break, cf.
<a class="moz-txt-link-freetext" href="http://isabelle.in.tum.de/testboard/Isabelle/report/edd1df5c8daf4109a6366801aaeff7fd">http://isabelle.in.tum.de/testboard/Isabelle/report/edd1df5c8daf4109a6366801aaeff7fd</a><br>
(Some errors are due to your changes, some are due to current work
of others.)<br>
It might be good to provide some patches for the AFP to have a
smooth transition.<br>
<br>
<br>
Lukas<br>
<br>
<br>
On 04/04/2012 09:20 AM, Christian Sternagel wrote:
<blockquote cite="mid:4F7BF63A.5060204@jaist.ac.jp" type="cite">Hi
all,
<br>
<br>
On 03/31/2012 01:10 AM, Florian Haftmann wrote:
<br>
<blockquote type="cite">
<blockquote type="cite">PS: I suggest to rename "rel_comp" into
"relcomp" (to be consistent with
<br>
"relpow").
<br>
</blockquote>
<br>
This would also mean to rename the corresponding lemmas,
although I
<br>
would also appreciate consistency. Also the »pred_comp«
abbreviation
<br>
should be dropped, with the subsequent consequences for theorem
names.
<br>
This would also be something you could contribute if you like.
<br>
</blockquote>
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.)
<br>
<br>
cheers
<br>
<br>
chris
<br>
<br>
<fieldset class="mimeAttachmentHeader"></fieldset>
<br>
<pre wrap="">_______________________________________________
isabelle-dev mailing list
<a class="moz-txt-link-abbreviated" href="mailto:isabelle-dev@in.tum.de">isabelle-dev@in.tum.de</a>
<a class="moz-txt-link-freetext" href="https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev">https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev</a>
</pre>
</blockquote>
<br>
</body>
</html>