- Installed specific code generator for equality enforcing that arguments do not have function types, which would result in an error message during compilation. - Added test case generators for basic types.

added upd_fst, upd_snd, some thms

added map_image, restrict_map, some thms

added fold_red, o2l, postfix, some thms

added rev_ballE

re-introduced sort constraints on LHS

corrected markup text

Changed many Intersection rules from i:I to I~=0 to avoid introducing a new variable

~= to neq

converting more theories to Isar scripts, and tidying

Conversion of ZF/UNITY/{FP,Union} to Isar script. Introduction of X-symbols to the ML files.

A patch by david aspinall

Added check for HOL_proofs: Theory WeakNorm is skipped if HOL image has been compiled without proof objects.

converted UNITY/Comp/{AllocImpl,Client} to Isar scripts

converted Counter, Counterc and PriorityAux to Isar scripts (all HOL/UNITY/Comp)

Conversion of UNITY/Comp/Priority.thy to a linear Isar script

Type antiquotations do not use the bracket syntax by default any longer.

moved some lemmas here from ZF

Removal of UNITY/UNITYMisc, moving its theorems elsewhere. Conversion of UNITY/State to Isar format.;

Added DOCTYPE and Content-type to HTML documents.

Moved function for renaming bound variables to Pure/drule.ML

Added functions for renaming bound variables.

Added split_paired_All rule for splitting variables bound by object-level universal quantifiers.

- record_split_tac now also works for object-level universal quantifier - bound variables in split rule now have nicer names - added new simproc record_eq_simproc which prevents simplifier from choosing the "wrong" equality rule

integrated optimizations by Sebastian Skalberg, produces less garbage, is faster and clearer

Conversion of theory UNITY to Isar script

Conversion of AllocBase to new-style

*** empty log message ***

*** empty log message ***

Conversion of "Merge" to Isar format