<html><head><meta http-equiv="Content-Type" content="text/html charset=iso-8859-1"></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space;">Joe,<div><br><div><div>On 18 Mar 2014, at 17:49, Joe Leslie-Hurd <<a href="mailto:joe@gilith.com">joe@gilith.com</a>> wrote:</div><br class="Apple-interchange-newline"><blockquote type="cite"><div dir="ltr">Hi Rob,<div><br></div><div>The HOLLight.* symbols are "auxiliary" type operators and constants that are used in proofs but not exported by any theory. So it's not unreasonable that it is defined multiple times in subtheories of base. However, what is surprising is that the article compression algorithm implemented in the opentheory tool does not fold the multiple definitions into a single definition.</div> <div><br></div><div>Thanks for the report: I'll look into the problem. This code will need reworking anyway to process the new article commands.</div><div><br></div><div>If the multiple definitions are causing problems then as a workaround you can pick an arbitrary new name for any symbols in the HOLLight namespace, because such symbols are guaranteed never to be appear in any exported theorem.</div></div></blockquote><div><br></div>Thanks for that, it may come in useful. It will only work if the repeated definitions all give alpha-equivalent defining properties.</div><div><br></div><div>I think the article format definition should specify whether redefinition is allowed (and I would vote strongly for a constraint forbidding redefinition).</div><div><br></div></div><div>Regards,</div><div><br></div><div>Rob.</div><div><br></div></body></html>