some uses of "' " as witness for this feature;

tuned declarations for more compact proof terms;

isabelle update -u path_cartouches;

isabelle update -u control_cartouches;

isabelle update -u mixfix_cartouches;

simplified ZF theory names (in contrast to 6a0801279f4c): session-qualification already achieves disjointness;

--HG--
rename : src/ZF/Datatype_ZF.thy => src/ZF/Datatype.thy
rename : src/ZF/Inductive_ZF.thy => src/ZF/Inductive.thy
rename : src/ZF/Int_ZF.thy => src/ZF/Int.thy
rename : src/ZF/IntDiv_ZF.thy => src/ZF/IntDiv.thy
rename : src/ZF/List_ZF.thy => src/ZF/List.thy
rename : src/ZF/Nat_ZF.thy => src/ZF/Nat.thy

avoid undeclared frees;

isabelle update_cartouches -c -t;

tuned syntax -- more symbols;

fewer aliases for toplevel theorem statements;

isabelle update_cartouches;

slightly more formal historic examples;

modernized header;

discontinued old "xnum" token category;
simplified Lexicon.read_num, Lexicon.read_float: no sign here;
express ZF numerals via "num" with mixfix grammar;
recovered printing of ZF numerals: "one" is abbreviation;

integrated appendix theory into main theory;
tuned ML

--HG--
extra : rebase_source : a066b231916d8839dd4199f5a608ee49e36e9fd9

prefer ML_file over old uses;

replacing ":" by "\<in>"

Using mathematical notation for <-> and cardinal arithmetic

mathematical symbols instead of ASCII

renamed inner syntax categories "num" to "num_token" and "xnum" to "xnum_token";

modernized structures;

numeral syntax: clarify parse trees vs. actual terms;
modernized translations;
formal markup of @{syntax_const} and @{const_syntax};

eliminated hard tabulators, guessing at each author's individual tab-width;
tuned headers;

tuned ML code, more antiquotations;

Made theory names in ZF disjoint from HOL theory names to allow loading both developments
in a single session (but not merge them).

modernized specifications;
removed legacy ML bindings;

moved Integ files to canonical place;