Next: Module Types
Up: Theories
Previous: Adding Set Definitions
Nuprl abstractions can be used to provide notational abbreviations
for ML. A couple of current abstractions for ML add common suffices
to tactics.
- (T ...) is an abbreviation for T THEN Auto.
An editor command
C-.
t, given when at a text cursor when
editing ML, inserts this abbreviation and leaves a text cursor at the
internal slot for the argument T.
- Similarly, (T ...a) is an abbreviation for T THENA Auto,
and the appropriate editor command is
C-.
a.
Karla Consroe
Wed Oct 23 13:48:45 EDT 1996