Library ML Functions

  These functions are all most commonly typed in at the ML Top-Loop. One is free to define abbreviations or alternative ML functions in terms of these primitives The functions take the following kinds of arguments:

obname 

An ML string. The name of an object. Acceptable names are composed from the alphabet a-zA-Z0-9_ . The first character should be a letter.

place 

An ML string. The name of an object. The library position understood is immediately before the object named. ` last ` may be used to refer to a fictitious object after the last object in library.

n

A non-negative number.

()

This is the unique inhabitant of the ML type unit.

Remember that ML strings  are always enclosed in "

characters, and that ML functions are always terminated by ;; . Some commands take lists as arguments; ML Lists  are delimited by []'s and use ; to separate items.

• Library Window Motion
• Library Editing
• Theory Commands