tuned whitespace

tuned headings

avoid open

tuned internal structure

fail on merge of conflicting normalization entries: functions are not mergable

more canonical data administration

removed former algebra presimpset entirely

removed former algebra presimpset from accessor

removed former algebra presimpset from signature

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;