<html><head></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space; "><div>I have a couple of problems with hol light implementation of Open Theory.</div><div><br></div><div>I followed the instructions at <a href="http://src.gilith.com/hol-light.html">http://src.gilith.com/hol-light.html</a>, but got lots of errors when I tried to load opentheory/all.ml. The problem was a syntax error caused by a missing semi-colon in theorems.ml (see patch below).</div><div><br></div><div>When I fixed that, opentheory/all.ml loaded without any errors. From a glance at the source, I expected interesting things to appear in opentheory/articles, but there was nothing. What have I missed?</div><div><br></div><div>Regards,</div><div><br></div><div>Rob.</div><div><br></div><div><div>--- theorems.ml-<span class="Apple-tab-span" style="white-space:pre"> </span>2013-07-31 11:33:20.000000000 +0100</div><div>+++ theorems.ml<span class="Apple-tab-span" style="white-space:pre"> </span>2013-07-31 11:33:25.000000000 +0100</div><div>@@ -426,7 +426,7 @@</div><div> </div><div> export_thm EXISTS_REFL;;</div><div> </div><div>-let EXISTS_REFL' = ONCE_REWRITE_RULE [EQ_SYM_EQ] EXISTS_REFL;</div><div>+let EXISTS_REFL' = ONCE_REWRITE_RULE [EQ_SYM_EQ] EXISTS_REFL;;</div><div> </div><div> let EXISTS_UNIQUE_REFL = prove</div><div> (`!a:A. ?!x. x = a`,</div></div><div><br></div></body></html>