isabelle update -u path_cartouches;

isabelle update -u control_cartouches;

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

more symbols;

isabelle update_cartouches -c -t;

isabelle update_cartouches;

modernized header;

modernized setup;

prefer ML_file over old uses;

declare command keywords via theory header, including strict checking outside Pure;

replacing ":" by "\<in>"

Using mathematical notation for <-> and cardinal arithmetic

mathematical symbols instead of ASCII

modernized some old-style infix operations, which were left over from the time of ML proof scripts;

eliminated obsolete "standard";

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

modernized specifications;
removed legacy ML bindings;

migrated theory headers to new format

tuned dependencies;

Groups, Rings and supporting lemmas

new case_tac

more new-style theories

various new lemmas for Constructible

Removal of mono.thy

improved presentation markup

conversion of many files to Isar format

moved rulify to ObjectLogic;

tuned ML code (the_context, bind_thms(s));

installation of cancellation simprocs for the integers

new typechecking solver for the simplifier

obselete 'end' hack;

Moved definitions (binary intersection, etc.) from upair.thy back to ZF.thy

Implicit simpsets and clasets for FOL and ZF

made pseudo theories for all ML files;
documented dependencies between all thy and ML files