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;
2014-04-15 wenzelm 2014-04-15 NEWS;
2014-04-12 wenzelm 2014-04-12 NEWS;
2014-04-11 wenzelm 2014-04-11 explicit 'document_files' in session ROOT specifications; clarified Isabelle_System.copy_file(_base): preserve file-attributes and local directory hierarchy;
2014-04-10 wenzelm 2014-04-10 NEWS;
2014-04-09 wenzelm 2014-04-09 allow text cartouches in regular outer syntax categories "text" and "altstring";
2014-04-07 wenzelm 2014-04-07 refrain from changing jEdit default shortcuts, due to potential for conflicts and actually not working on Mac OS X;
2014-04-06 wenzelm 2014-04-06 renamed "isabelle-process" to "isabelle_process", with shell function to avoid dynamic path lookups;
2014-04-04 wenzelm 2014-04-04 support for jEdit Navigator plugin;
2014-04-04 wenzelm 2014-04-04 added ML antiquotation @{print};
2014-04-03 hoelzl 2014-04-03 merged DERIV_intros, has_derivative_intros into derivative_intros
2014-04-02 hoelzl 2014-04-02 extend continuous_intros; remove continuous_on_intros and isCont_intros
2014-04-02 hoelzl 2014-04-02 moved generic theorems from Complex_Analysis_Basic; fixed some theorem names
2014-03-31 wenzelm 2014-03-31 cumulative NEWS;
2014-03-27 wenzelm 2014-03-27 clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler;
2014-03-26 wenzelm 2014-03-26 tuned;
2014-03-25 wenzelm 2014-03-25 proper configuration option "ML_print_depth"; proper ML_exception_trace for HOL-TPTP;
2014-03-25 wenzelm 2014-03-25 clarified options ML_source_trace and ML_exception_trace (NB: the latter needs to be a system option, since the context is sometimes not available, e.g. for 'theory' command);
2014-03-25 wenzelm 2014-03-25 some SML examples;
2014-03-25 wenzelm 2014-03-25 added command 'SML_file' for Standard ML without Isabelle/ML add-ons;
2014-03-24 wenzelm 2014-03-24 discontinued Toplevel.debug in favour of system option "exception_trace";
2014-03-22 haftmann 2014-03-22 generalized and strengthened cong rules on compound operators, similar to 1ed737a98198
2014-03-21 wenzelm 2014-03-21 more qualified names;
2014-03-20 wenzelm 2014-03-20 more static checking of proof methods;
2014-03-19 haftmann 2014-03-19 elongated INFI and SUPR, to reduced risk of confusing theorems names in the future while still being consistent with INTER and UNION
2014-03-19 hoelzl 2014-03-19 NEWS
2014-03-18 haftmann 2014-03-18 consolidated theorem names containing INFI and SUPR: have INF and SUP instead uniformly
2014-03-18 wenzelm 2014-03-18 clarified modules; more antiquotations for antiquotations;
2014-03-16 haftmann 2014-03-16 normalising simp rules for compound operators
2014-03-15 haftmann 2014-03-15 more complete set of lemmas wrt. image and composition