Re: [isabelle] ML functions
On Fri, 23 Sep 2011, Steve Wong wrote:
I have two questions regarding implementing ML functions:
1) If I have a file containing my own ML function "foo" in a structure
"bar", I seem to have to call "bar" using "foo.bar". I see that the
functions in BasicLibrary, Term, etc., one could call "maps" by just "maps"
and not "BasicLibrary.maps". So how should "bar" be defined in order to be
able to call "foo" with just "foo"?
The idea is to wrap things in structures by default, and only make parts
of the content pervasive later, either by 'open' of a substructure or by
individual 'val' declarations after the structure definition. Here are
some representative examples for both ways:
See the start and end of these files, respectively.
2) If my functions spread over numerous files, is there a neat way for
including all these files in a .thy rather than 10 or so individual
lines of 'use "..."'?
10 'use' commands are not so much -- we do this routinely with many more
You can also embed ML text directly in the theory body, using the 'ML'
command, or variations of it.
This archive was generated by a fusion of
Pipermail (Mailman edition) and