[opentheory-users] Problems with the hol light Open Theory support
Joe Leslie-Hurd
joe at gilith.com
Wed Jul 31 20:59:02 UTC 2013
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
>
More information about the opentheory-users
mailing list