1999-10-30 wenzelm 1999-10-30 tuned;
1999-10-30 wenzelm 1999-10-30 isabellesym.sty;
1999-10-30 wenzelm 1999-10-30 definitions of many Isabelle symbols;
1999-10-29 wenzelm 1999-10-29 final update by Gertrud Bauer;
1999-10-29 wenzelm 1999-10-29 workaround bug (feature?) in bibtex;
1999-10-29 wenzelm 1999-10-29 tuned;
1999-10-29 wenzelm 1999-10-29 comment out isabellesym.sty;
1999-10-29 wenzelm 1999-10-29 improved;
1999-10-29 wenzelm 1999-10-29 \isasymbol renamed to \isasym;
1999-10-29 wenzelm 1999-10-29 tuned;
1999-10-29 wenzelm 1999-10-29 tuned msg;
1999-10-29 wenzelm 1999-10-29 \isasym;
1999-10-29 oheimb 1999-10-29 improved singleton_insert_inj_eq
1999-10-28 wenzelm 1999-10-28 improved presentation;
1999-10-28 wenzelm 1999-10-28 fixed deps;
1999-10-28 wenzelm 1999-10-28 tuned;
1999-10-28 paulson 1999-10-28 expandshort; tidied
1999-10-28 paulson 1999-10-28 localTo_imp_o_localTo is now really an implication
1999-10-28 paulson 1999-10-28 simplified the stable_completion proofs
1999-10-28 paulson 1999-10-28 tidied
1999-10-28 paulson 1999-10-28 expandshort
1999-10-28 wenzelm 1999-10-28 improved IsarThy.init_context;
1999-10-28 wenzelm 1999-10-28 tuned;
1999-10-27 oheimb 1999-10-27 added various little lemmas
1999-10-27 oheimb 1999-10-27 clarsimp_tac now copes with the (unwanted) case that the simplifier splits the goal
1999-10-27 wenzelm 1999-10-27 tuned msg;
1999-10-27 wenzelm 1999-10-27 tuned;
1999-10-27 wenzelm 1999-10-27 added (try_)update_thy_only; added (try_)context_thy_only command;
1999-10-27 wenzelm 1999-10-27 added init_context;
1999-10-27 wenzelm 1999-10-27 quiet_update_thy: ml flag; replaced broken del_deps by upd_deps; begin_theory: better handling of 'files';
1999-10-27 nipkow 1999-10-27 Fixed a bug in the EX simproc.
1999-10-27 wenzelm 1999-10-27 export cond_with_path;
1999-10-27 wenzelm 1999-10-27 dummy_pattern: aprop;
1999-10-27 wenzelm 1999-10-27 updated for Isabelle99;
1999-10-27 paulson 1999-10-27 working again; new treatment of LocalTo
1999-10-27 paulson 1999-10-27 TEMPORARY use of Addsimps
1999-10-27 paulson 1999-10-27 got rid of split_diff, which duplicated nat_diff_split, and also disposed of remove_diff_ss
1999-10-27 oheimb 1999-10-27 symbols in (error) messages now consistently with single backslash
1999-10-27 oheimb 1999-10-27 now more than 256 generated bound variables possible
1999-10-27 oheimb 1999-10-27 reset_goals no longer empties the proof stack
1999-10-26 wenzelm 1999-10-26 improved ml handling; tuned;
1999-10-26 wenzelm 1999-10-26 improved ml handling;
1999-10-26 wenzelm 1999-10-26 tuned; always ml_prompts;
1999-10-26 wenzelm 1999-10-26 activate ml_prompts;
1999-10-26 wenzelm 1999-10-26 added inform_file_processed, inform_file_retracted; proper outer syntax setup; more robust theory loader actions;
1999-10-26 wenzelm 1999-10-26 added kill_proof_notify;
1999-10-26 wenzelm 1999-10-26 added check_known_thy, if_known_thy; simplified loaded_files;
1999-10-26 wenzelm 1999-10-26 Isabelle %f;
1999-10-26 wenzelm 1999-10-26 do not set proof_timing;
1999-10-26 wenzelm 1999-10-26 export kill_theory;
1999-10-26 wenzelm 1999-10-26 added kill_thy;
1999-10-26 wenzelm 1999-10-26 added opt_unit (from isar_syn.ML);
1999-10-26 wenzelm 1999-10-26 added drop_ext; tuned;
1999-10-25 wenzelm 1999-10-25 improved handling of warn_extra_tfrees;
1999-10-25 wenzelm 1999-10-25 update by Gertrud Bauer;
1999-10-25 wenzelm 1999-10-25 added Real/HahnBanach/document/root.bib;
1999-10-22 wenzelm 1999-10-22 warn_extra_tfrees (after declare_term);
1999-10-22 wenzelm 1999-10-22 warn_extra_tfrees; removed bind(_i), add_binds, declare_term;
1999-10-22 wenzelm 1999-10-22 warn_extra_tfrees;
1999-10-22 wenzelm 1999-10-22 tuned repeat_undo;