NEWS
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;
2014-02-17 ago updated NEWS
2014-02-16 ago folded 'rel_option' into 'option_rel'
2014-02-16 ago folded 'list_all2' with the relator generated by 'datatype_new'
2014-02-16 ago more NEWS
2014-02-12 ago [mq]: news
2014-02-10 ago discontinued axiomatic 'classes', 'classrel', 'arities';
2014-02-04 ago interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
2014-02-04 ago removed legacy 'metisFT' method
2014-02-03 ago renamed 'smt' option 'smt_proofs' to avoid clash with 'smt' prover
2014-02-03 ago added new option to documentation
2014-01-30 ago renamed Sledgehammer options for symmetry between positive and negative versions
2014-01-26 ago discontinued obsolete attribute "standard";
2014-01-25 ago explicit eigen-context for attributes "where", "of", and corresponding read_instantiate, instantiate_tac;