1999-07-30 wenzelm 1999-07-30 Isabelle/Isar macros;
1999-07-30 wenzelm 1999-07-30 hacking the rail package;
1999-07-30 wenzelm 1999-07-30 added update_thy_only; moved update_thy;
1999-07-30 wenzelm 1999-07-30 more;
1999-07-30 wenzelm 1999-07-30 more stuff;
1999-07-30 wenzelm 1999-07-30 renamed 'same' to '-';
1999-07-30 wenzelm 1999-07-30 eliminated METHOD0 in favour of same_tac;
1999-07-30 wenzelm 1999-07-30 'arith' proof method;
1999-07-30 wenzelm 1999-07-30 added erule; renamed same to -;
1999-07-30 wenzelm 1999-07-30 export sysify_path;
1999-07-30 paulson 1999-07-30 split_diff and remove_diff_ss
1999-07-29 paulson 1999-07-29 added parentheses to cope with a possible reduction of the precedence of unary minus
1999-07-28 wenzelm 1999-07-28 ML_HOME=$ISABELLE_HOME/../smlnj/bin;
1999-07-28 wenzelm 1999-07-28 HOL-Real target now builds an actual image;
1999-07-28 wenzelm 1999-07-28 added pretty_setmargin;
1999-07-28 paulson 1999-07-28 congruence rule for |-, etc.
1999-07-28 paulson 1999-07-28 renamed ...thm_pack... to ...pack...
1999-07-28 paulson 1999-07-28 removed the unused SeqVar option
1999-07-28 paulson 1999-07-28 sequents require higher bounds
1999-07-28 paulson 1999-07-28 more examples are working
1999-07-28 paulson 1999-07-28 adding missing declarations for the <<...>> notation
1999-07-28 paulson 1999-07-28 congruence rule for |-
1999-07-28 paulson 1999-07-28 simplifier and improved classical reasoner
1999-07-28 wenzelm 1999-07-28 mkdir contrib;
1999-07-28 paulson 1999-07-28 added String.concat
1999-07-28 paulson 1999-07-28 LK
1999-07-27 wenzelm 1999-07-27 back again, supposedly with correct perms;
1999-07-27 wenzelm 1999-07-27 *** empty log message ***
1999-07-27 wenzelm 1999-07-27 fixed perms and final nl;
1999-07-27 wenzelm 1999-07-27 fixed comments;
1999-07-27 wenzelm 1999-07-27 fixed comment;
1999-07-27 wenzelm 1999-07-27 inductive_cases(_i): Isar interface to mk_cases;
1999-07-27 wenzelm 1999-07-27 safe_step_tac / step_tac;
1999-07-27 wenzelm 1999-07-27 init / init_theory: pass int flag;
1999-07-27 wenzelm 1999-07-27 added thy_switch kind;
1999-07-27 wenzelm 1999-07-27 removed update_context; context / theory: proper update in interactive mode;
1999-07-27 wenzelm 1999-07-27 removed update_context; removed restart; added init_toplevel, touch_all_thys, touch_thy, remove_thy, update_thy_only;
1999-07-27 wenzelm 1999-07-27 removed restart; added touch_all_thys, touch_thy, remove_thy, update_thy_only;
1999-07-27 wenzelm 1999-07-27 setup_thy_loader;
1999-07-27 wenzelm 1999-07-27 added update_thy_only; added theory loader action hook; added touch_all_thys; touch_thy: all_succs;
1999-07-27 paulson 1999-07-27 installation of simplifier and classical reasoner, better rules etc
1999-07-27 paulson 1999-07-27 moved the modal prover to modal.ML; installed the prover using TheoryDataFun
1999-07-27 paulson 1999-07-27 split off modal.ML from provers.ML
1999-07-27 paulson 1999-07-27 fixed the comments...
1999-07-27 paulson 1999-07-27 a new theory containing just an axiom needed to derive imp_cong
1999-07-27 paulson 1999-07-27 renamed theory LK to LK0
1999-07-27 paulson 1999-07-27 renamed LK0.ML
1999-07-27 paulson 1999-07-27 Sequents/LK/Nat: new example of simplification in LK
1999-07-27 paulson 1999-07-27 added gen_inter
1999-07-27 paulson 1999-07-27 expandshort and tidying
1999-07-27 paulson 1999-07-27 expandshort; tidied
1999-07-27 paulson 1999-07-27 tidied
1999-07-26 paulson 1999-07-26 expandshort
1999-07-26 paulson 1999-07-26 HOL/ex/Tarski: new example by Florian Kammueller
1999-07-26 paulson 1999-07-26 new facts about binomials
1999-07-26 paulson 1999-07-26 three new theorems
1999-07-26 paulson 1999-07-26 new cancellation laws
1999-07-26 paulson 1999-07-26 tidied
1999-07-23 paulson 1999-07-23 new simprocs assoc_fold and combine_coeff
1999-07-23 paulson 1999-07-23 removed the combine_coeff simproc because linear arith does not handle coefficients yet