more basic replacement of newlines;

static Symbol.spaces;

proper use of var stopped;

removed junk;

tuned headers;

tuned;

merged

merged

moved normalization proof tool infrastructure to canonical algebraic classes

added lemmas

merged

renamed Normalizer to the more specific Semiring_Normalizer

delete Groebner_Basis directory -- only one file left

split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces

merged

moved lemma zdvd_period to theory Int

tuned;

discontinued Pretty.setdepth, which appears to be largely unused, but can disrupt important markup if enabled accidentally;

tuned error message: regular Pretty.string_of instead of raw Pretty.output;

unified/simplified Pretty.margin_default; discontinued special Pretty.setmargin etc; explicit margin argument for Pretty.string_of_margin etc.;

renamed Thm.get_name -> Thm.derivation_name and Thm.put_name -> Thm.name_derivation, to emphasize the true nature of these operations;

prefer Thm.get_name_hint, which is closer to a user-space idea of "theorem name";

tuned signature;

added of_sort_proof according to krauss/schropp, with slightly more direct canonical_instance;

back-patching of axclass proofs;

back-patching via Single_Assignment.var;

support several sidekick parsers -- very basic default parser;

sidekick: unformatted content, notably without newlines;

unformatted output;

output symbolic pretty printing markup and format in the front end;

Pretty.formatted operates directly on XML trees, treating XML.Elem like a pro-forma block of indentation 0, like the ML version; tuned;

tuned;

strip_shyps_proof: dummy TFrees are called "'dummy" as in del_conflicting_tvars below;

use existing undefined function;

merged

removed semicolons

rule subrelI (for nice Isar proofs of relation inequalities)

merged

merged

prefix normalizing replaces class_semiring

xsymbolized

moved method syntax here

tuned proof

former free-floating field_comp_conv now in structure Normalizer

proper sublocales; no free-floating ML sections

moved some lemmas from Groebner_Basis here

revert to loose merge semantics

merged