improved ml handling;

tuned; always ml_prompts;

activate ml_prompts;

added inform_file_processed, inform_file_retracted; proper outer syntax setup; more robust theory loader actions;

added kill_proof_notify;

added check_known_thy, if_known_thy; simplified loaded_files;

Isabelle %f;

do not set proof_timing;

export kill_theory;

added kill_thy;

added opt_unit (from isar_syn.ML);

added drop_ext; tuned;

improved handling of warn_extra_tfrees;

update by Gertrud Bauer;

added Real/HahnBanach/document/root.bib;

warn_extra_tfrees (after declare_term);

warn_extra_tfrees; removed bind(_i), add_binds, declare_term;

warn_extra_tfrees;

tuned repeat_undo;

debug_simp;

new flag debug_simp

tuned simplifier trace output; new flag debug_simp

achieve proper italic correction;

HahnBanach update by Gertrud Bauer;

replaced image_image_eq_UN by image_eq_UN

ALMOST working version: LocalTo results commented out

new default simprules for UN and INT

new theorems on Image

tidied using modern infix form

tuned trace_action;

added known_thy; added touch_child_thys; tuned loaded_files;

end/kill_theory: check_known_thy;

added touch_child_thys;

\isakeyword: fixed italic correction;

get_thm;

tuned;

proper handling of axioms / defs;

markup: keep indentation;

added is_indent;

export thy_path;

output \isasymbols;

forall_elim_var(s) move here from drule.ML; add_axioms/defs: forall_elim_vars on result;

forall_elim_var(s) moved to pure_thy.ML;

*** empty log message ***

removed \BG, \EN;

updated;

added \ISS;

eliminated isar_action;

remove_thy: warn unknown theory (rather than error);

use_mltext: better control of verbosity;

use_text: remove last char from output;

option -m TARGET;

removed -B option;

tuned usage;

the settings environment is now statically scoped; tuned;

fixed update_thy_only;