tuned;

clarified signature: more operations;

merged

clarified signature;

tuned names/scopes;

tuned signature: more operations;

eliminate historic clone (see also 550e36c6a2d1);

tuned signature: more operations;

clarified 'unbundle' polarity, according to algebraic group laws;

tuned signature: more operations;

tuned: more direct use of Name.context operations;

tuned;

misc tuning and clarification: more direct use of Name.context operations;

tuned signature: more operations;

tuned: more direct use of Name.context operations;

clarified signature: shorten common cases;

tuned: more standard Name.build_context, although that is a bit longer;

clarified signature: more uniform;

omit redundant combinators (amending 7456a64bc4f6);

tuned signature;

fixed bugs found by Stepan Holub

merged

added lemmas

merged

more ambitious Search_Result.gui_text, using Swing HTML3 (NB: TreeCellRenderer cannot do this, because it is not updated for each entry);

clarified signature and object initialization;

clarified default: avoid copies;

suppress odd icons for documents and folders;

support for modified tree cell renderer;

clarified signature: avoid implicit functionality;

re-use Output_Area;

re-use Output_Area;

re-use Output_Area;

re-use Output_Area with search results;

re-use Output_Area with search results;

more thorough init;

clarified signature: prefer defaults for Output_Dockable (and its variants);

unused;

tuned output: formatting is pointless for proportional font;

clarified Tree_View.init_model: more uniform;

more robust update;

handle tree selection;

Output_Dockable: show search results as tree view;

clarified modules;

clarified signature;

clarified signature;

clarified signature and modules: without GUI change yet;

more operations, to support search within output panel;

tuned;

Introduced the function some_elem for grabbing an element from a non-empty set, and simplified the theorem the_elem_image_unique

Patch by Stepan Holub, plus tweaks

patch to vector_matrix_mult by Alexander Pach

try0: cleaned up output;

try0: insert extra facts into state instead of goal, since some methods (e.g. metis) won't work otherwise;

avoid informatik.tu-muenchen.de domain: soon to be discontinued;

renamed Discrete -> Discrete_Functions to avoid name clashes; new function names floor_log/sqrt to avoid long Discrete_Functions.log/sqrt

Use Var to maintain the difference between function and locale parameters

tuned

tuned proofs;

tuned proofs;