Commands.

In this index we describe all the commands. The index is divided in two sections: the top-level commands (always accepted) and the proof commands (accepted only when doing a proof).

• Top-level commands.
  • Control commands.
  • Commands modifying the theory.
  • Commands modifying proof commands.
  • Inductive definitions.
  • Managing files and modules.
  • TeX.
  • Obtaining some informations on the system.
  • Term-extraction.
  
  
• Proof commands.
  • Basic proof commands.
  • More proof commands.
  • Automatic proving.
  • Rewriting.
  • Managing existential variables.
  • Managing goals.
  • Managing context.
  • Managing state of the proof.
  • Tacticals.