[isabelle] ML functions


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"?

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 "..."'?



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.