Miscellaneous Functions

mm: tactic.

Prints a reasonable representation of the proof into the snapshot file without modifying the proof. It is intended to be used as a transfomation tactic.

term_to_tok: term tok.

Converts a term into a token representation.

print_term: term void.

Displays a term.

rule_to_tok: rule tok.

print_rule: rule void.

Displays a representation of a rule.

declaration_to_tok: declaration tok.

print_declaration: declaration void.

Displays a declaration.

main_goal_of_theorem: tok term.

Returns the term which is the conclusion of the top node of the named theorem.

extracted_term_of_theorem: tok term.

Returns the term extracted from the named theorem.

map_on_subterms: (term term) term term.

Replaces each immediate subterm of the term argument by the result of applying the function argument to it.

free_vars: term term list.

remove_illegal_tags: term term.

Takes a term and removes the smallest number of tags needed to make the term have a tagging which is legal with respect to the direct computation rules. (See appendix C for a definition of legal tagging.)

do_computations: term term.

Returns the result of performing the computations indicated by the tags in the argument. (See appendix C for a description of the direct computation rules).

no_extraction_compute: term term.

Computes (in the sense of the direct computation rules) the term as far as possible, without treating term_of terms as redices; these are treated in the same way as variables.

loadt: tok void.

Loads the named file into the ML environment. The name given must be the name, or path name, of the file, with the extension (e.g., `` .ml'') removed; the appropriate version (binary, Lisp or ML source) will be loaded. Note that ML written in files can only mention other ML objects; in particular, Nuprl \ definitions cannot be instantiated, and the single quote cannot be used to form Nuprl terms.

compilet: tok void.

Compiles the named file, putting the Lisp and binary code files in the same directory as the named file. The argument should be the full path name for the file with the extension removed.