2000-08-04 wenzelm dummy_pattern moved to term.ML;
2000-08-04 wenzelm Term.no_dummy_patterns;
2000-08-04 wenzelm added rev_eq_reflection;
2000-08-04 wenzelm val rev_eq_reflection = def_imp_eq;
2000-08-04 wenzelm val atomize = thms "atomize";
2000-08-04 wenzelm lemmas atomize = all_eq imp_eq;
2000-08-04 wenzelm rev_eq_reflection = meta_eq_to_obj_eq;
2000-08-04 wenzelm removed stac (now exported by HypsubstFun);
2000-08-04 wenzelm setup hypsubst_setup;
2000-08-04 wenzelm lemmas atomize = all_eq imp_eq;
2000-08-04 wenzelm added rev_eq_reflection;
2000-08-04 wenzelm subgoals_tac: fixed spelling;
2000-08-04 wenzelm invoke isatool make in any dir containing an IsaMakefile;
2000-08-04 wenzelm updated;
2000-08-04 wenzelm targets for images, test, all;
2000-08-04 wenzelm updated;
2000-08-04 wenzelm tuned;
2000-08-03 wenzelm tuned version by Stephan Merz (unbatchified etc.);
2000-08-03 wenzelm tuned TLA;
2000-08-03 wenzelm added setmp_verbose;
2000-08-03 wenzelm tuned;
2000-08-03 wenzelm unknown_theory/proof/context;
2000-08-03 wenzelm added unknown_theory/proof/context;
2000-08-03 paulson new theorem neq_commute
Loading...
(0) -3000 -1000 -300 -100 -50 -24 +24 +50 +100 +300 +1000 +3000 +10000 +30000 tip