History log of /seL4-l4v-master/HOL4/src/1/theory_tests/MLdepLib.sml
Revision Date Author Comments
# a86cc43e 07-Mar-2017 Michael Norrish <Michael.Norrish@nicta.com.au>

Provide fn for users to specify ML dependencies for theories

This will be useful when a theory wants to export a specific
pretty-printing or parsing function. For example, the special
printing of if-then-else is not properly exportable at the moment
because there is no way to capture it as a string in a theory file.

The ultimate intention is to give it a name in a special
dictionary, and to make the theory depend on ML code that implements
the function and inserts it into that dictionary under the user's
choice of name.