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;

updated;

recover original definitions of \isactrlsub etc.;

canonical interface for 'default'

output \<^loc> as 'loc' span; tuned;

isatool latex -o sty;

added 'loc';

updated;

ASCII back-quote no longer sym char;

added \isactrlloc;

* ML functions legacy_bindings and use_legacy_bindings;

avoid symbolic identifier;

added (use_)legacy_bindings;

output_basic: handle AltString token;

removed obsolete type_syn;

unskolem local vars;

tuned;

added alt_string;

added AltString token (delimited by ASCII back-quotes); ASCII back-quote no longer symbolic char;

removed unused dest operation;

export theorems_of;

tuned some proofs;

removed obsolete arities;

tuned size of included graph;

added \isachardoublequoteopen/close, \isacharbackquoteopen/close;

(branch cleanup)

(allocating new branch)

added superclasses, class_le_path

added alist.ML

added 'these', removed assoc2

added alist module

Fixed bug.

DFG output now works for untyped rules (ML "ResClause.untyped();")

Lemmas on dvd, power and finite summation added or strengthened.

replaced '?' by '??'

Adapted to new code generator syntax.