basic formatting of pretty trees; line-up ML vs. Scala sources;

added content_length;

slightly more general Library.chunks;

misc tuning -- accumulate body via ListBuffer;

basic support for symbolic pretty printing; tuned;

extractors for document updates; Session.handle_result: use extractors instead of raw patterns -- NB: using mixed patterns of case classes vs. extractors crashes Scala 2.8.1 RC1;

extractors for outer keyword declarations;

eliminated deprecated "--" method; use case classes with copy method for functional record update;

use IndexedSeq instead of deprecated RandomAccessSeq, which is merely an alias;

use SwingApplication instead of deprecated GUIApplication;

simplified via Position extractors;

some rearrangement of Scala sources;

fminus and some more theorems ported from Finite_Set.

eq_morphism is always optional: avoid trivial morphism for empty list of equations

tuned whitespace

tuned interpunctation, dropped dead comment

merged

avoid using '...' with LIMSEQ (cf. 1cc4ab4b7ff7)

generalize some lemmas to class t1_space

simplify definition of t1_space; generalize lemma closed_sing and related lemmas

generalize some lemmas

convert comments to 'text' blocks

generalize more lemmas about limits

repaired comments where SOMEthing went utterly wrong (cf. 2b04504fcb69)

merged

generalize types of LIMSEQ and LIM; generalize many lemmas

make (f -- a --> x) an abbreviation for (f ---> x) (at a)

make (X ----> L) an abbreviation for (X ---> L) sequentially