March 2001

Completed Proof Witness Extraction.
Added Sequents with Type Conclusions, Sequents with Restricted Declarations.
Reworked Sequents a bit punting to Sequents with Type Conclusions.
Mentioned polymorphism and gave an example in Intersection Types
Added Propositions as Types - standard defs which really needs support from further explanations.
Alluded to Comprehension Subtypes and Quotient Types in Types.
Described equality between quotient type expressions in Quotient Types and alluded to it in Intensional Types.
Reordered entries in primitive op doc INDEX to make it closer to order of understanding.
Made some of the structure of the Operator Definition document explicit.
Improved the wording in Evaluation and Term Rewriting about marking subterms for rewriting.
In NonCanonical Forms, removed the <term> marks, and added mention of principal argument place.
In Terms, added an example of 2-place snd-o var instance, and deleted line about creation of new expressions.
Reworded Russell's Orders to make it clear that a sequence of orders was being described.
Eliminated from Equality references to props as types.
Added some detailed reminders to previous info Type Expressions.
Added mention of typing Kleene's mu operator to Recursive Functions.
Some subtypes of were mentioned in Integers.

Feb 2001

The bulk of the documentation, down to but excluding computational content of propositions and choice principles, written in February 2001. Citations are to be added later. Here are the documents then considered complete:

Pairs	Boolean
Atoms	Negative Literals
Disjoint Union	Deriving Bool
Lists	Unit
Void	Deriving Unit
Integers	Recursive Functions
Quotient Types	Recursion via the Y-combinator
Comprehension Subtypes	Y-combinator Continued
Equality	Multi-argument Functions with Y
Intersection Types	Recursive Types
Guarded Types	Terms
Types	Operator Definition
Intensional Types	Op Def Restrictions
Computation	Substitution
Evaluation and Term Rewriting	Canonical Forms
Universes	NonCanonical Forms
Propositions	Type Expressions
Functions	Proofs
Function Types	Propositions as Types
Multi-Argument Functions	Prop Levels and Predicativity
Functionality Sequents	Higher-Order Propositions
Sequents	ML
Type Functionality Sequents	Russell's Orders

The incomplete documents these refer to are Choice(incomplete) and Computational Content(incomplete).

About: IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html