Contents
  Acknowledgements
 1.  Introduction
   1.1.  Simultaneous free algebras
   1.2.  Partial continuous functionals
   1.3.  Primitive recursion, computable functionals
   1.4.  Decidable predicates, axioms for predicates
   1.5.  Minimal logic, proof transformation
   1.6.  Comparison with Coq and Isabelle
 2.  Types, with simultaneous free algebras as base types
   2.1.  Generalitites for substitutions, type substitutions
   2.2.  Simultaneous free algebras as base types
 3.  Variables
 4.  Constants
   4.1.  Rewrite and computation rules for program constants
   4.2.  Recursion over simultaneous free algebras
   4.3.  Internal representation of constants
 5.  Predicate variables and constants
   5.1.  Predicate variables
   5.2.  Predicate constants
   5.3.  Inductively defined predicate constants
 6.  Terms and objects
   6.1.  Normalization
   6.2.  Substitution
 7.  Formulas and comprehension terms
 8.  Assumption variables and constants
   8.1.  Assumption variables
   8.2.  Axiom constants
   8.3.  Theorems
   8.4.  Global assumptions
 9.  Proofs
   9.1.  Constructors and accessors
   9.2.  Normalization
   9.3.  Substitution
   9.4.  Display
   9.5.  Classical logic
 10.  Interactive theorem proving with partial proofs
   10.1.  Partial proofs
   10.2.  Interactive theorem proving
 11.  Search
 12.  Computational content of classical proofs
 13.  Extracted terms
 14.  Reading formulas in external form
   14.1.  Lexical analysis
   14.2.  Parsing
References
Index