Additional BigO lemmas that require the HOL-Complex logic image;

added copy-dump option;

added line break for 'uses';

added no_body_context;

use_dir: added copy-dump option;

present_text: Toplevel.no_body_context prevents use of wrong context in interaction;

refer to theory instead of low-level tsig; use Thm.full_prop_of instead of Thm.prop_of; tuned use of map/filter/fold;

tuned classes_arities_of;

refer to theory instead of low-level tsig;

added Avigad-Donnelly;

reactivate postfix by change of syntax; tuned presentation;

tuned presentation;

moved lemmas that require the HOL-Complex logic image to Complex/ex/BigO_Complex.thy; tuned presentation;

added Complex/ex/BigO_Complex.thy;

simp_implies: proper named infix;

tuned;

isatool usedir: added option -C;

added option -C: copy existing document directory;

* Delimiters of outer tokens now produce separate LaTeX macros; * isatool usedir: option -C (default true) controls copying of document directory;

introduced AList.*

better map_entry

fixed bug in record_type_abbr_tr'

patterns in setsum and setprod

Updated import.

updated;

delimiter markup for verbatim tokens;

clarify type tok, do not emit markup flag for suppressed tokens;

use AList operations;

cover tagged command regions; tuned;

tune spacing where a generated theory text is included directly;