reactivated other_id reports (see also db929027e701, 8eda56033203);

invisible context similar to interpretation;

avoid massive multiplication of reports due to interpretation;

tuned comments;

more thorough update;

several updates on polynomial long division and pseudo division - division of polynomials is now available on idom_divide (was field before) - added polynomial pseudo division (on comm_ring_1) - improved code equation for polynomial (pseudo)-division (joint work of S. Joosten, R. Thiemann, and A. Yamada)

fragment of a HOL type class primer

capitalized GCD and LCM syntax

environment variable check has become pointless after 771b8ad5c7fc

unfold internal definitions before emitting a proof obligation

more IDE support for Isabelle/Pure bootstrap;

merged

tuned signature;

prefer internal attribute source;

tidying some proofs; getting rid of "nonempty_witness"

Merge

numerous theorems about affine hulls, hyperplanes, etc.

merged

proper LaTeX;

tuned;

clarified bindings;

clarified bindings;

tuned;

tuned;

avoid clash with function called "x";

new theorems about convex hulls, etc.; also, renamed some theorems

clarified bindings;

clarified bindings;

prefer binding over base name;

clarified signature;