[Push:] This command takes two string arguments. The theorem named by the first argument is ``pushed'' into the module associated with the theorem named by the second argument.
[Open:] This command takes a single string argument. The tactic module named by the argument is opened.
[Close:] This command takes a single string argument. The tactic module named by the argument is closed.
[PopModule:] This command takes a single argument. The tactic module named by the argument is ``popped'' and all theorems in the module are copied into the current module.
[CloseAll:] This command takes a unit argument. All tactic modules are closed.