NEWS
2014-07-04 wenzelm 2014-07-04 misc tuning for release;
2014-07-04 wenzelm 2014-07-04 NEWS;
2014-07-02 wenzelm 2014-07-02 tuned grammar and spelling (cf. 0cf15843b82f);
2014-07-01 immler 2014-07-01 overdue NEWS concerning c4daa97ac57a
2014-07-01 paulson 2014-07-01 for new release
2014-07-01 wenzelm 2014-07-01 misc updates for release;
2014-06-30 wenzelm 2014-06-30 ProofGeneral-4.2-2 is optional component (including the traditional helper scripts);
2014-06-30 wenzelm 2014-06-30 "isabelle tty" is superseded by "isabelle console";
2014-06-30 haftmann 2014-06-30 qualified String.explode and String.implode
2014-06-29 blanchet 2014-06-29 killed Python version of MaSh, now that the SML version works adequately
2014-06-28 haftmann 2014-06-28 tracing facilities for the code generator preprocessor
2014-06-28 wenzelm 2014-06-28 updated NEWS -- removed material that is already in the manual;
2014-06-28 haftmann 2014-06-28 fact consolidation
2014-06-27 wenzelm 2014-06-27 command 'print_term_bindings' supersedes 'print_binds';
2014-06-27 wenzelm 2014-06-27 removed obsolete "isabelle unsymbolize";
2014-06-18 blanchet 2014-06-18 enabled MaSh by default -- set 'MaSh' to 'none' in Isabelle Plugin Options to disable
2014-06-13 paulson 2014-06-13 NEWS
2014-06-13 hoelzl 2014-06-13 properties of normal distributed random variables (by Sudeep Kanav)
2014-06-13 nipkow 2014-06-13 announce Tree
2014-06-12 blanchet 2014-06-12 tuning
2014-06-12 blanchet 2014-06-12 renamed Sledgehammer options
2014-06-12 blanchet 2014-06-12 updated docs
2014-06-12 blanchet 2014-06-12 took out broken support for Yices from SMT2 stack -- see 'NEWS' for rationale
2014-06-11 blanchet 2014-06-11 updated NEWS slightly
2014-05-29 nipkow 2014-05-29 removed Kleene_Algebra because of superior AFP entry; authors agreed
2014-05-27 blanchet 2014-05-27 don't generate discriminators and selectors for 'datatype_new' unless the user asked for it
2014-05-26 blanchet 2014-05-26 got rid of '=:' squiggly
2014-05-26 blanchet 2014-05-26 renamed 'MaSh' option
2014-05-24 wenzelm 2014-05-24 support for regular Windows TeX installation;
2014-05-20 blanchet 2014-05-20 added naive Bayes ML implementation, due to Cezary Kaliszyk (like k-NN)
2014-05-20 blanchet 2014-05-20 added Isabelle system option 'mash'
2014-05-20 blanchet 2014-05-20 news
2014-05-19 hoelzl 2014-05-19 renamed positive_integral to nn_integral
2014-05-19 hoelzl 2014-05-19 introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
2014-05-15 haftmann 2014-05-15 type
2014-05-13 traytel 2014-05-13 bnf_decl -> bnf_axiomatization
2014-05-12 wenzelm 2014-05-12 NEWS;
2014-05-09 haftmann 2014-05-09 hardcoded nbe and sml into value command
2014-05-09 haftmann 2014-05-09 prefer separate command for approximation
2014-05-07 wenzelm 2014-05-07 NEWS;
2014-05-07 hoelzl 2014-05-07 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
2014-05-06 wenzelm 2014-05-06 renamed "Find" to "Query", with more general operations;
2014-05-04 blanchet 2014-05-04 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 blanchet 2014-05-04 added 'satx' proof method to Try0
2014-05-04 blanchet 2014-05-04 renamed 'xxx_size' to 'size_xxx' for old datatype package
2014-05-04 boehmes 2014-05-04 removed obsolete internal SAT solvers
2014-05-03 wenzelm 2014-05-03 support for path completion based on file-system content;
2014-05-02 wenzelm 2014-05-02 merged
2014-05-02 wenzelm 2014-05-02 NEWS;
2014-05-02 haftmann 2014-05-02 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 boehmes 2014-05-01 added internal proof-producing SAT solver
2014-05-01 haftmann 2014-05-01 NEWS
2014-04-29 wenzelm 2014-04-29 require explicit 'document_files';
2014-04-26 wenzelm 2014-04-26 merged
2014-04-26 wenzelm 2014-04-26 NEWS;
2014-04-26 kleing 2014-04-26 retired wwwfind
2014-04-23 blanchet 2014-04-23 updated NEWS
2014-04-19 wenzelm 2014-04-19 added command 'SML_export' and 'SML_import' for exchange of toplevel bindings;
2014-04-15 wenzelm 2014-04-15 more NEWS;
2014-04-15 wenzelm 2014-04-15 clarified abbreviations for cartouche delimiters, to work in any context;