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

[Joe Leslie-Hurd]

Hi Rob,

Sorry for the broken state of the repo - I really should set up a
work-in-progress branch and only push to master when it's in a
consistent state.

To export a single theory from the proof logging fork of HOL Light,
follow the instructions at

http://www.gilith.com/research/opentheory/faq.html#export-from-hol-light

The initial start_logging command is used to switch on proof logging,
which is off by default since most users don't want to export the
whole standard theory library.

However, that may indeed be exactly what you want, in which case carry
out the following two steps:

cd opentheory
make theories

Then you should see a lot of stuff pile up in opentheory/articles/

Hope that helps,

Joe

On Wed, Jul 31, 2013 at 4:12 AM, Rob Arthan <rda at lemma-one.com> wrote:
> 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`,
>
>
> _______________________________________________
> opentheory-users mailing list
> opentheory-users at gilith.com
> http://www.gilith.com/opentheory/mailing-list
>