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
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