ML Functions for ML Top Loop

**Table 3:** Functions for ML Top Loop
`up` n	Scroll up n lines
`down` n	Scroll down n lines
`top ()`	Jump to top of library
`bottom ()`	Jump to bottom of library
`create_thm` name place	create theorem
`view name`	view theorem (or other library object)

`add_theory_delimiters` thy	add new theory to library
`set_theory_filename` thy fname	assoc theory to file
`dump_theory` thy	write theory to file
`load_theory` thy	load theory from file
`print_theory` thy	print `.prl` and `.tex` files

The most important ML-Top-Loop functions are summarized in Table 3. Notes on functions:

name, place, thy and fname should be enclosed in $\ulcorner$ " $\urcorner$ 's.

name and and thy should all use only alphanumeric characters and underscore ( $\ulcorner$ $\urcorner$ ). place should start with + or - to indicate position immediately before or after the object named.

fname should include a full pathname but no extension. Files:

fname.prl text file with special characters.
fname.tex L^ATEX file for input to latex.
fname.dvi Output file from L^ATEX.
fname.thy theory file. (Lisp Expressions).

Tactics

Up:

Reference Material for Tutorial

Proof Editor

Dora Abdullah, 12/4/97