Hi Bill,
You can overwrite the OCaml exception printer if you want, like I do in HOL
Zero in 'exn.ml' and the main build file 'holzero.ml', where the error
message is part of the exception and gets printed out if/when the exception
bubbles to the top. You could do something like this:
let pri
Hi Ramana,
On Fri, Jul 26, 2013 at 10:42 AM, Ramana Kumar wrote:
> Is it possible to add newly defined/proved constants and theorems to the
> database used by this service, so it can be used to prove lemmas in a
> development in progress?
>
So far you have to do your own local install for that,
Vince, I figured out how to print error messages without double-quotes and with
actual newlines! This and a lot more is explained in the ocaml doc in "Module
Format", which I got the idea to use after looking at Freek's miz3.ml. I'd like
to get rid of a trailing message Exception: Failure "".
This looks really nice. Well done.
On Thu, Jul 25, 2013 at 5:01 PM, Vincent Aravantinos <
vincent.aravanti...@gmail.com> wrote:
> Hi list,
>
> I recently gave a tutorial about HOL internals here in Concordia and I
> though it might be useful to share with the community, in case anyone is
> inter
Is it possible to add newly defined/proved constants and theorems to the
database used by this service, so it can be used to prove lemmas in a
development in progress?
On Fri, Nov 30, 2012 at 5:29 PM, Josef Urban wrote:
> Automated reasoning service using about 16000 Flyspeck (and HOL
> Light)
