Contents

• Introduction.
  • Motivation.
  • Actual state.
  • Other sources of documentation
  
  
• Emacs and XEmacs interface.
  • Getting things to work.
  • Getting started.
  • Tips.
  • Other definitions
  
  
• Examples
  • How to read the examples.
  • An example in analysis
  
  
• Expressions, parsing and pretty printing.
  • Notations.
  • Lexical analysis.
  • Sorts
  • Syntax
  • Expressions
  • Commands
  
  
• Natural Commands
  • Examples
  • The syntax of the command
  • Semantics
  
  
• The module system
  • Basic principles
  • Compiling and importing
  • Renaming and using
  • Exported or not exported?
  • Multiple modules in one file
  
  
• Inductive predicates and data-types.
  • Inductive predicates.
  • Inductive data-types.
  
  
• Generation of LaTeX documents.
  • The LaTeX header.
  • LaTeX comments.
  • Producing formulas
  • Multi-line formulas
  • User defined LaTeX syntax.
  • examples.
  
  
• Installation.
• Commands.
  • 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.
  
  
• Flags index.
• Bibliography