NEWS
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
2014-03-31 ago cumulative NEWS;
2014-03-27 ago clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler;
2014-03-26 ago tuned;
2014-03-25 ago proper configuration option "ML_print_depth";
2014-03-25 ago 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 ago some SML examples;
2014-03-25 ago added command 'SML_file' for Standard ML without Isabelle/ML add-ons;
2014-03-24 ago discontinued Toplevel.debug in favour of system option "exception_trace";
2014-03-22 ago generalized and strengthened cong rules on compound operators, similar to 1ed737a98198
2014-03-21 ago more qualified names;
2014-03-20 ago more static checking of proof methods;
2014-03-19 ago 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 ago NEWS
2014-03-18 ago consolidated theorem names containing INFI and SUPR: have INF and SUP instead uniformly
2014-03-18 ago clarified modules;
2014-03-16 ago normalising simp rules for compound operators
2014-03-15 ago more complete set of lemmas wrt. image and composition
2014-03-14 ago merged
2014-03-13 ago added ML antiquotation @{path};
2014-03-14 ago updated NEWS and CONTRIBUTORS (BNF, SMT2, Sledgehammer)
2014-03-13 ago dropped redundant theorems
2014-03-13 ago enhanced simplifier solver for preconditions of rewrite rule, can now deal with conjunctions
2014-03-12 ago tuned signature -- clarified module name;
2014-03-12 ago added ML antiquotation @{here};
2014-03-12 ago simplified programming interface to define ML antiquotations -- NB: the transformed context ignores updates of the context parser;
2014-03-06 ago merged
2014-03-06 ago some NEWS;
2014-03-06 ago renamed 'fun_rel' to 'rel_fun'
2014-03-06 ago renamed 'prod_rel' to 'rel_prod'
2014-03-06 ago renamed 'sum_rel' to 'rel_sum'
2014-03-06 ago renamed 'filter_rel' to 'rel_filter'