tuned;

expandshort; tidied

localTo_imp_o_localTo is now really an implication

simplified the stable_completion proofs

tidied

expandshort

improved IsarThy.init_context;

tuned;

added various little lemmas

clarsimp_tac now copes with the (unwanted) case that the simplifier splits the goal

tuned msg;

tuned;

added (try_)update_thy_only; added (try_)context_thy_only command;

added init_context;

quiet_update_thy: ml flag; replaced broken del_deps by upd_deps; begin_theory: better handling of 'files';

Fixed a bug in the EX simproc.

export cond_with_path;

dummy_pattern: aprop;

updated for Isabelle99;

working again; new treatment of LocalTo

TEMPORARY use of Addsimps

got rid of split_diff, which duplicated nat_diff_split, and also disposed of remove_diff_ss

symbols in (error) messages now consistently with single backslash

now more than 256 generated bound variables possible

reset_goals no longer empties the proof stack

improved ml handling; tuned;

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;

qed_spec_mp is a mess;

tuned;

tuned;

update by Stephan Merz;

exchanged the first two args of "project" and "drop_prog"

fixed comments

working version with localTo[C] instead of localTo

new thm disjoint_iff_not_equal

new thm vimage_image_eq

PROOFGENERAL_OPTIONS="-u false";

improved presentation;

fixed comment;

Removed obsolete comment.

Documented thm_deps.

Corrected typo.

improved presentation;

support thumbpdf;

fixed comment;

pdf: generate thumbnails if ISABELLE_THUMBPDF set;

support thumbpdf (via 'png' output format);

thumbpdf (disabled by default);

document preparation based on (PDF)LaTeX;

renamed verbatim/verb to text_raw/txt_raw;

tuned;

improved presentation;

berghofe;

isabelle-isar-ref;

tuned usage;

-d pdf;

system; use_text: pass print function;

use_text_verbose;

system;

markup / varbatim: comment out (%) newline char;

use_text writeln;

mkdir, copy_all: system_command;

updated;

Eliminated mutual_induct_tac.

Eliminated mutual_induct_tac.