tuned document; tuned proofs;
eliminated some generated comments;
be explicit about .ML files;
added Statespace library