2010-05-08 wenzelm 2010-05-08 back-patching via Single_Assignment.var;
2010-05-07 wenzelm 2010-05-07 support several sidekick parsers -- very basic default parser;
2010-05-07 wenzelm 2010-05-07 sidekick: unformatted content, notably without newlines;
2010-05-07 wenzelm 2010-05-07 unformatted output;
2010-05-07 wenzelm 2010-05-07 output symbolic pretty printing markup and format in the front end;
2010-05-07 wenzelm 2010-05-07 Pretty.formatted operates directly on XML trees, treating XML.Elem like a pro-forma block of indentation 0, like the ML version; tuned;
2010-05-07 wenzelm 2010-05-07 tuned;
2010-05-07 wenzelm 2010-05-07 strip_shyps_proof: dummy TFrees are called "'dummy" as in del_conflicting_tvars below;
2010-05-07 wenzelm 2010-05-07 use existing undefined function;
2010-05-07 wenzelm 2010-05-07 merged
2010-05-07 krauss 2010-05-07 removed semicolons
2010-05-07 krauss 2010-05-07 rule subrelI (for nice Isar proofs of relation inequalities)
2010-05-07 wenzelm 2010-05-07 merged
2010-05-07 haftmann 2010-05-07 merged
2010-05-07 haftmann 2010-05-07 prefix normalizing replaces class_semiring
2010-05-06 haftmann 2010-05-06 xsymbolized
2010-05-06 haftmann 2010-05-06 moved method syntax here
2010-05-06 haftmann 2010-05-06 tuned proof
2010-05-06 haftmann 2010-05-06 former free-floating field_comp_conv now in structure Normalizer
2010-05-06 haftmann 2010-05-06 proper sublocales; no free-floating ML sections
2010-05-06 haftmann 2010-05-06 moved some lemmas from Groebner_Basis here
2010-05-06 haftmann 2010-05-06 revert to loose merge semantics
2010-05-06 haftmann 2010-05-06 merged
2010-05-06 haftmann 2010-05-06 moved generic lemmas to appropriate places
2010-05-06 haftmann 2010-05-06 tuned
2010-05-06 haftmann 2010-05-06 dropped duplicate comp_arith
2010-05-06 haftmann 2010-05-06 avoid open; tuned references to theorems
2010-05-06 haftmann 2010-05-06 avoid references to groebner bases in names which have no references to groebner bases
2010-05-06 haftmann 2010-05-06 tuned whitespace
2010-05-06 haftmann 2010-05-06 tuned headings
2010-05-06 haftmann 2010-05-06 avoid open
2010-05-06 haftmann 2010-05-06 tuned internal structure
2010-05-06 haftmann 2010-05-06 fail on merge of conflicting normalization entries: functions are not mergable
2010-05-06 haftmann 2010-05-06 more canonical data administration
2010-05-06 haftmann 2010-05-06 removed former algebra presimpset entirely
2010-05-06 haftmann 2010-05-06 removed former algebra presimpset from accessor
2010-05-06 haftmann 2010-05-06 removed former algebra presimpset from signature
2010-05-06 haftmann 2010-05-06 moved presimplification rules for algebraic methods into named thms functor
2010-05-06 haftmann 2010-05-06 tuned whitespace; dropped superfluous open
2010-05-06 haftmann 2010-05-06 dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
2010-05-05 haftmann 2010-05-05 moved nat_arith ot Nat_Numeral: clarified normalizer setup
2010-05-05 haftmann 2010-05-05 dropped unused file
2010-05-05 haftmann 2010-05-05 dropped Id
2010-05-06 huffman 2010-05-06 remove unused constant preal_of_rat; remove several unused lemmas about preals
2010-05-06 Cezary Kaliszyk 2010-05-06 respectfullness and preservation of prod_rel
2010-05-06 haftmann 2010-05-06 ProofContext.init_global
2010-05-06 haftmann 2010-05-06 merged
2010-05-05 haftmann 2010-05-05 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 =)
2010-05-06 haftmann 2010-05-06 constant name access lattice is not in use any longer
2010-05-06 wenzelm 2010-05-06 uniform treatment of length = 1 for forced breaks, also makes ML/Pretty.length coincide with Scala/XML.content_length;
2010-05-06 wenzelm 2010-05-06 replaced slightly odd fbreak markup by plain "\n", which also coincides with regular linebreaks produced outside the ML pretty engine;
2010-05-06 wenzelm 2010-05-06 added separate;
2010-05-06 wenzelm 2010-05-06 basic formatting of pretty trees; line-up ML vs. Scala sources;
2010-05-06 wenzelm 2010-05-06 added content_length;
2010-05-06 wenzelm 2010-05-06 slightly more general Library.chunks;
2010-05-06 wenzelm 2010-05-06 misc tuning -- accumulate body via ListBuffer;
2010-05-06 wenzelm 2010-05-06 basic support for symbolic pretty printing; tuned;
2010-05-06 wenzelm 2010-05-06 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;
2010-05-06 wenzelm 2010-05-06 extractors for outer keyword declarations;
2010-05-05 wenzelm 2010-05-05 eliminated deprecated "--" method; use case classes with copy method for functional record update;