Next:
Contents
Contents
The Proof checker Documentation
Version 0.85
Christophe Raffalli
LAMA, Université de Savoie
March 2, 2005
Paul Rozière
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.
Blanks
Comments
String, numbers, ...
Identifiers
Special characters
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
About this document ...
Christophe Raffalli 2005-03-02
