2000-08-11 kleing 2000-08-11 added LBV
2000-08-11 paulson 2000-08-11 new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
2000-08-11 paulson 2000-08-11 ZF arith
2000-08-11 paulson 2000-08-11 interim working version: more improvements to the integers
2000-08-10 berghofe 2000-08-10 Equations that are added to the simpset now have proper names.
2000-08-10 paulson 2000-08-10 new structure field "add" for CombineNumerals
2000-08-10 paulson 2000-08-10 the "nocheck" versions of goal functions now standardize their result
2000-08-10 paulson 2000-08-10 tidied
2000-08-10 paulson 2000-08-10 new structure field "add" for CombineNumerals
2000-08-10 paulson 2000-08-10 installation of cancellation simprocs for the integers
2000-08-10 wenzelm 2000-08-10 X-Symbol mode -- look in canonical place;
2000-08-09 wenzelm 2000-08-09 fixed spelling;
2000-08-09 wenzelm 2000-08-09 added Bauer-Wenzel:2000:HB;
2000-08-09 wenzelm 2000-08-09 thms closure;
2000-08-09 wenzelm 2000-08-09 res_inst: include non-inst versions with multiple thms; ML tactic: thms closure; tuned msgs;
2000-08-09 wenzelm 2000-08-09 added get_thms_closure, single_thm;
2000-08-09 wenzelm 2000-08-09 fixed classification of rules in atts and modifiers (final!?);
2000-08-09 wenzelm 2000-08-09 fixed mk_cases_i: TRYALL InductMethod.simp_case_tac;
2000-08-09 wenzelm 2000-08-09 thms "atomize";
2000-08-09 bauerg 2000-08-09 tuned;
2000-08-09 kleing 2000-08-09 tuned
2000-08-08 wenzelm 2000-08-08 token translation: enclose "\\mbox{" "}";
2000-08-08 oheimb 2000-08-08 added Example
2000-08-08 oheimb 2000-08-08 moved Hoare_example to Examples; other minor improvements
2000-08-08 berghofe 2000-08-08 Deleted unneeded proof; simplified proof of app_last.
2000-08-08 wenzelm 2000-08-08 added forall_elim_vars_safe, norm_hhf_eq;
2000-08-08 wenzelm 2000-08-08 norm_hhf results;
2000-08-08 wenzelm 2000-08-08 prf_heading kind;
2000-08-07 kleing 2000-08-07 MicroJava structure changed
2000-08-07 kleing 2000-08-07 Invoke instruction gets fully qualified method name (class+name+sig) as in Sun's JVM spec
2000-08-07 kleing 2000-08-07 BV and LBV specified in terms of app and step functions
2000-08-07 paulson 2000-08-07 instantiated Cancel_Numerals for "nat" in ZF
2000-08-07 paulson 2000-08-07 more cterm operations: mk_implies, list_implies
2000-08-07 paulson 2000-08-07 prove_conv gets an extra argument, so the ZF instantiation can use hyps
2000-08-07 paulson 2000-08-07 tidied
2000-08-07 paulson 2000-08-07 added a dummy "thm list" argument to prove_conv for the new interface to Cancel_Numerals
2000-08-07 paulson 2000-08-07 new abstract syntax operations, used in ZF
2000-08-07 paulson 2000-08-07 ZF arith
2000-08-06 nipkow 2000-08-06 *** empty log message ***
2000-08-04 wenzelm 2000-08-04 dummy_patterns moved to term.ML;
2000-08-04 wenzelm 2000-08-04 added goal_args('); added "cut_tac", "thin_tac", "rename_tac"; renamed inst tactics; inst syntax: include empty inst;
2000-08-04 wenzelm 2000-08-04 added int;
2000-08-04 wenzelm 2000-08-04 axioms: Term.no_dummy_patterns;
2000-08-04 wenzelm 2000-08-04 added dummy_patternN, no_dummy_patterns, replace_dummy_patterns;
2000-08-04 wenzelm 2000-08-04 added rename_params_tac;
2000-08-04 wenzelm 2000-08-04 dummy_pattern moved to term.ML;
2000-08-04 wenzelm 2000-08-04 Term.no_dummy_patterns;
2000-08-04 wenzelm 2000-08-04 added rev_eq_reflection; export stac; proof method setup: subst, hypsubst;
2000-08-04 wenzelm 2000-08-04 val rev_eq_reflection = def_imp_eq;
2000-08-04 wenzelm 2000-08-04 val atomize = thms "atomize";
2000-08-04 wenzelm 2000-08-04 lemmas atomize = all_eq imp_eq; setup hypsubst_setup;
2000-08-04 wenzelm 2000-08-04 rev_eq_reflection = meta_eq_to_obj_eq;
2000-08-04 wenzelm 2000-08-04 removed stac (now exported by HypsubstFun);
2000-08-04 wenzelm 2000-08-04 setup hypsubst_setup;
2000-08-04 wenzelm 2000-08-04 lemmas atomize = all_eq imp_eq;
2000-08-04 wenzelm 2000-08-04 added rev_eq_reflection;
2000-08-04 wenzelm 2000-08-04 subgoals_tac: fixed spelling;
2000-08-04 wenzelm 2000-08-04 invoke isatool make in any dir containing an IsaMakefile;
2000-08-04 wenzelm 2000-08-04 updated;
2000-08-04 wenzelm 2000-08-04 targets for images, test, all;