[MLton] HOL's Moscow ML implementation, and pushing MLton to emulate it

[Stephen Weeks]

> I'd really like to write
> 
>   val ADD_COMM = DB "arithmetic" "ADD_COMM"
>   fun solve_system s = .... ADD_COM ....
> 
> But this won't work because the binding for ADD_COMM will happen as
> the executable starts up, in an arithmetic-free context, and DB will
> raise an exception.  (We need to support such a context precisely so
> that our tool can itself be used for the development of the arithmetic
> theory in the first place). 

I don't understand the problem with this approach.  Why can't you
guarantee that the DB has the necessary theorem, either from an
earlier invocation of a different executable, or earlier in the
startup of this executable?