2010-05-09 krauss 2010-05-09 added lemmas rel_comp_UNION_distrib(2)
2010-05-08 wenzelm 2010-05-08 made SML/NJ happy;
2010-05-09 wenzelm 2010-05-09 reactivated Thm.legacy_unconstrainT for Nbe.lift_triv_classes_conv;
2010-05-09 wenzelm 2010-05-09 Thm.unconstrainT based on Logic.unconstrainT -- no proofterm yet;
2010-05-09 wenzelm 2010-05-09 just one version of Thm.unconstrainT, which affects all variables; temporary workaround for Nbe.lift_triv_classes_conv;
2010-05-09 wenzelm 2010-05-09 added Logic.unconstrain_allTs, based on calculations_for_thm_proof by krauss/schropp, but treat type variables uniformly as in strip_shyps (in thm.ML) or stripped_sorts (in more_thm.ML);
2010-05-09 wenzelm 2010-05-09 tuned;
2010-05-09 wenzelm 2010-05-09 removed unused "option" variants of "same" operations;
2010-05-09 wenzelm 2010-05-09 more basic replacement of newlines;
2010-05-09 wenzelm 2010-05-09 static Symbol.spaces;
2010-05-08 wenzelm 2010-05-08 proper use of var stopped;
2010-05-08 wenzelm 2010-05-08 removed junk;
2010-05-08 wenzelm 2010-05-08 tuned headers;
2010-05-08 wenzelm 2010-05-08 tuned;
2010-05-08 wenzelm 2010-05-08 merged
2010-05-08 haftmann 2010-05-08 merged
2010-05-08 haftmann 2010-05-08 moved normalization proof tool infrastructure to canonical algebraic classes
2010-05-08 nipkow 2010-05-08 added lemmas
2010-05-08 haftmann 2010-05-08 merged
2010-05-07 haftmann 2010-05-07 renamed Normalizer to the more specific Semiring_Normalizer
2010-05-07 haftmann 2010-05-07 delete Groebner_Basis directory -- only one file left
2010-05-07 haftmann 2010-05-07 split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
2010-05-07 haftmann 2010-05-07 merged
2010-05-07 haftmann 2010-05-07 moved lemma zdvd_period to theory Int
2010-05-08 wenzelm 2010-05-08 tuned;
2010-05-08 wenzelm 2010-05-08 discontinued Pretty.setdepth, which appears to be largely unused, but can disrupt important markup if enabled accidentally;
2010-05-08 wenzelm 2010-05-08 tuned error message: regular Pretty.string_of instead of raw Pretty.output;
2010-05-08 wenzelm 2010-05-08 unified/simplified Pretty.margin_default; discontinued special Pretty.setmargin etc; explicit margin argument for Pretty.string_of_margin etc.;
2010-05-08 wenzelm 2010-05-08 renamed Thm.get_name -> Thm.derivation_name and Thm.put_name -> Thm.name_derivation, to emphasize the true nature of these operations;
2010-05-08 wenzelm 2010-05-08 prefer Thm.get_name_hint, which is closer to a user-space idea of "theorem name";
2010-05-08 wenzelm 2010-05-08 tuned signature;
2010-05-08 wenzelm 2010-05-08 added of_sort_proof according to krauss/schropp, with slightly more direct canonical_instance;
2010-05-08 wenzelm 2010-05-08 back-patching of axclass proofs;
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