...primitives

The user should consult the ML file commands.ml for details on writing his or her own library functions.

...taken

and which others have taken too, for example in the Cornell Synthesizer-Generator  project

...side

For example, it can be useful to define an abstraction that has some typing information associated with it, but that unfolds to a term without that information

...meta-terms

The meta-parameters are different from those used in abstraction definitions. To be clear, we sometimes call those ones abstraction-meta-variables  and the ones in display definitions, display-meta-variables  .

...aux.

main is currently used as both a class name, and a particular label name, so there is currently no way to select only subgoals in class main with label main.

...rem

Currently simplification involving 788#788 and rem isn't working

Karla Consroe
Wed Oct 23 13:48:45 EDT 1996