avoid undeclared frees;

isabelle update_cartouches;

prefer tactics with explicit context;

proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
occasionally clarified use of context;

proper context for assume_tac (atac remains as fall-back without context);

modernized header;

prefer 'named_theorems' over Named_Thms, with subtle change of semantics due to visual order vs. internal reverse order;

proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
clarified tool context in some boundary cases;

simplifier uses proper Proof.context instead of historic type simpset;

More mathematical symbols for ZF examples

eliminated obsolete "standard";

tuned Named_Thms: proper binding;

proper Proof.context for classical tactics;
reduced claset to snapshot of classical context;
discontinued clasimpset;

more antiquotations;
eliminated legacy ML bindings;

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

renamed simpset_of to global_simpset_of, and local_simpset_of to simpset_of -- same for claset and clasimpset;

renamed NamedThmsFun to Named_Thms;
simplified/unified names of instances of Named_Thms;

simplified method setup;

unified type Proof.method and pervasive METHOD combinators;

modernized specifications;
removed legacy ML bindings;

replaced program_defs_ref by proper context data (via attribute "program");

tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);

rewrite_goal_tac;

reorganized structure Goal vs. Tactic;

simplified method setup;

renamed "constrains" to "safety" to avoid keyword clash

conversion of UNITY to Isar scripts

updating ZF-UNITY with Sidi's new material

*** empty log message ***

new ZF/UNITY theory