2014-06-28 ago fact consolidation
2014-06-27 ago command 'print_term_bindings' supersedes 'print_binds';
2014-06-27 ago removed obsolete "isabelle unsymbolize";
2014-06-18 ago enabled MaSh by default -- set 'MaSh' to 'none' in Isabelle Plugin Options to disable
2014-06-13 ago NEWS
2014-06-13 ago properties of normal distributed random variables (by Sudeep Kanav)
2014-06-13 ago announce Tree
2014-06-12 ago tuning
2014-06-12 ago renamed Sledgehammer options
2014-06-12 ago updated docs
2014-06-12 ago took out broken support for Yices from SMT2 stack -- see 'NEWS' for rationale
2014-06-11 ago updated NEWS slightly
2014-05-29 ago removed Kleene_Algebra because of superior AFP entry; authors agreed
2014-05-27 ago don't generate discriminators and selectors for 'datatype_new' unless the user asked for it
2014-05-26 ago got rid of '=:' squiggly
2014-05-26 ago renamed 'MaSh' option
2014-05-24 ago support for regular Windows TeX installation;
2014-05-20 ago added naive Bayes ML implementation, due to Cezary Kaliszyk (like k-NN)
2014-05-20 ago added Isabelle system option 'mash'
2014-05-20 ago news
2014-05-19 ago renamed positive_integral to nn_integral
2014-05-19 ago introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
2014-05-15 ago type
2014-05-13 ago bnf_decl -> bnf_axiomatization
2014-05-12 ago NEWS;
2014-05-09 ago hardcoded nbe and sml into value command
2014-05-09 ago prefer separate command for approximation
2014-05-07 ago NEWS;
2014-05-07 ago avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
2014-05-06 ago renamed "Find" to "Query", with more general operations;
2014-05-04 ago renamed 'dpll_p' to 'cdclite', to avoid confusion with the old 'dpll' and to reflect the idea that the new prover implements some ideas from CDCL not in DPLL -- this follows its author's, Sascha B.'s, wish
2014-05-04 ago added 'satx' proof method to Try0
2014-05-04 ago renamed 'xxx_size' to 'size_xxx' for old datatype package
2014-05-04 ago removed obsolete internal SAT solvers
2014-05-03 ago support for path completion based on file-system content;
2014-05-02 ago merged
2014-05-02 ago NEWS;
2014-05-02 ago enforce case of identifiers only to accomodate strict language requirements (or clear separation of constructors from variables in the case of SML)
2014-05-01 ago added internal proof-producing SAT solver
2014-05-01 ago NEWS
2014-04-29 ago require explicit 'document_files';
2014-04-26 ago merged
2014-04-26 ago NEWS;
2014-04-26 ago retired wwwfind
2014-04-23 ago updated NEWS
2014-04-19 ago added command 'SML_export' and 'SML_import' for exchange of toplevel bindings;
2014-04-15 ago more NEWS;
2014-04-15 ago clarified abbreviations for cartouche delimiters, to work in any context;
2014-04-15 ago NEWS;
2014-04-12 ago NEWS;
2014-04-11 ago explicit 'document_files' in session ROOT specifications;
2014-04-10 ago NEWS;
2014-04-09 ago allow text cartouches in regular outer syntax categories "text" and "altstring";
2014-04-07 ago refrain from changing jEdit default shortcuts, due to potential for conflicts and actually not working on Mac OS X;
2014-04-06 ago renamed "isabelle-process" to "isabelle_process", with shell function to avoid dynamic path lookups;
2014-04-04 ago support for jEdit Navigator plugin;
2014-04-04 ago added ML antiquotation @{print};
2014-04-03 ago merged DERIV_intros, has_derivative_intros into derivative_intros
2014-04-02 ago extend continuous_intros; remove continuous_on_intros and isCont_intros
2014-04-02 ago moved generic theorems from Complex_Analysis_Basic; fixed some theorem names