isabelle update -u control_cartouches;

moved remaining display.ML to more_thm.ML;

more explicit context;

clarified Drule.gen_all: observe context more carefully;

tuned signature -- prefer qualified names;

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);

proper context for match_tac etc.;

more qualified names;

misc tuning and modernization;

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

more qualified names;
more antiquotations;

avoid stepping outside of context -- plain zero_var_indexes should be sufficient;

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

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

tuned signature;

simplified/unified Simplifier.mk_solver;

clarified map_simpset versus Simplifier.map_simpset_global;

more antiquotations

proper context for rule_by_tactic;

proper context for mksimps etc. -- via simpset of the running Simplifier;

removed old CVS Ids;
tuned headers;

renamed Simplifier.theory_context to Simplifier.global_context to emphasize that this is not the real thing;

renamed old-style Drule.standard to Drule.export_without_context, to emphasize that this is in no way a standard operation;

explicitly qualify Drule.standard;

more @{theory} antiquotations;

proper context for Display.pretty_thm etc. or old-style versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;

converted ML proofs from simpdata.ML;
tuned;

structure Display: less pervasive operations;

tuned ML setup;

removed legacy ML setup;

converted legacy ML scripts;

Simplifier.theory_context;

change_claset/simpset;

converted to Isar theory format;

renamed forall_elim_vars_safe to gen_all;

replace gen_all by forall_elim_vars_safe;

cong setup now part of Simplifier;

removal of batch style, and tidying

Mod because of new solver interface.

congruence rule for |-, etc.

installation of simplifier and classical reasoner, better rules etc