moved presimplification rules for algebraic methods into named thms functor

tuned whitespace; dropped superfluous open

dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML

moved nat_arith ot Nat_Numeral: clarified normalizer setup

dropped unused file

dropped Id

remove unused constant preal_of_rat; remove several unused lemmas about preals

respectfullness and preservation of prod_rel

ProofContext.init_global

merged

farewell to old-style mem infixes -- type inference in situations with mem_int and mem_string should provide enough information to resolve the type of (op =)

constant name access lattice is not in use any longer

uniform treatment of length = 1 for forced breaks, also makes ML/Pretty.length coincide with Scala/XML.content_length;

replaced slightly odd fbreak markup by plain "\n", which also coincides with regular linebreaks produced outside the ML pretty engine;

added separate;

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