Log Message: 
Numerous minor changes.
Added itt_fset: a theory of finite sets based on a list
implementation quotiented by equivalence under arbitrary
occurrences and ordering.
Added initial reflection theory. Terms are quotiented by
alphaequality, so normal wellformedness proofs are difficult,
and more work needs to be done to define free variables and
substitution.
