[opentheory-users] Problems with the hol light Open Theory support

[Rob Arthan]

I have a couple of problems with hol light implementation of Open Theory.

I followed the instructions at http://src.gilith.com/hol-light.html, 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).

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?

Regards,

Rob.

--- theorems.ml-	2013-07-31 11:33:20.000000000 +0100
+++ theorems.ml	2013-07-31 11:33:25.000000000 +0100
@@ -426,7 +426,7 @@
 
 export_thm EXISTS_REFL;;
 
-let EXISTS_REFL' = ONCE_REWRITE_RULE [EQ_SYM_EQ] EXISTS_REFL;
+let EXISTS_REFL' = ONCE_REWRITE_RULE [EQ_SYM_EQ] EXISTS_REFL;;
 
 let EXISTS_UNIQUE_REFL = prove
  (`!a:A. ?!x. x = a`,

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.gilith.com/opentheory/mailing-list/attachments/20130731/ffc0f954/attachment.html>