#
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.
|