isabelle update -u control_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;

clarified main ZF.thy / ZFC.thy, and avoid name clash with global HOL/Main.thy;

--HG--
rename : src/ZF/Main_ZF.thy => src/ZF/ZF.thy
rename : src/ZF/Main_ZFC.thy => src/ZF/ZFC.thy
rename : src/ZF/ZF.thy => src/ZF/ZF_Base.thy

isabelle update_cartouches -c -t;

isabelle update_cartouches;

tuned;

modernized header;

eliminated obsolete "standard";

eliminated global prems;

removed old CVS Ids;
tuned headers;

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

tuned induct proofs;

improved proofs;

migrated theory headers to new format

*** empty log message ***

clarified syntax of ``long'' statements: fixes/assumes/shows;

tuned document sources;

tuned;

isatool unsymbolize;

fixed;

added Term and Tree_Forest (from converted ZF/ex);