NEWS
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'
2014-03-06 ago renamed 'vset_rel' to 'rel_vset'
2014-03-06 ago fixed NEWS
2014-03-06 ago renamed 'set_rel' to 'rel_set'
2014-03-06 ago renamed 'cset_rel' to 'rel_cset'
2014-03-06 ago renamed 'fset_rel' to 'rel_fset'
2014-03-06 ago renamed 'map_sum' to 'sum_map'
2014-03-03 ago tuned code
2014-03-03 ago updated NEWS
2014-03-03 ago rationalized internals
2014-03-01 ago more precise imports;
2014-02-26 ago prefer proof context over background theory
2014-02-24 ago tuned;
2014-02-23 ago NEWS and documentation, including correction of long-overseen "*"
2014-02-23 ago dropped long-unused option
2014-02-22 ago NEWS;
2014-02-21 ago improved completion based on context information;
2014-02-21 ago NEWS
2014-02-20 ago clarified markup cumulation order (see also 25306d92f4ad and 0009a6ebc83b), e.g. relevant for completion_context;
2014-02-19 ago updated NEWS
2014-02-19 ago reflect 207538943038 in NEWS
2014-02-17 ago subtle change of semantics of Thm.eq_thm, e.g. relevant for merge of src/HOL/Tools/Predicate_Compile/core_data.ML (cf. HOL-IMP);
2014-02-17 ago NEWS;