NEWS
2014-03-15 haftmann 2014-03-15 more complete set of lemmas wrt. image and composition
2014-03-14 wenzelm 2014-03-14 merged
2014-03-13 wenzelm 2014-03-13 added ML antiquotation @{path};
2014-03-14 blanchet 2014-03-14 updated NEWS and CONTRIBUTORS (BNF, SMT2, Sledgehammer)
2014-03-13 haftmann 2014-03-13 dropped redundant theorems
2014-03-13 nipkow 2014-03-13 enhanced simplifier solver for preconditions of rewrite rule, can now deal with conjunctions
2014-03-12 wenzelm 2014-03-12 tuned signature -- clarified module name;
2014-03-12 wenzelm 2014-03-12 added ML antiquotation @{here};
2014-03-12 wenzelm 2014-03-12 simplified programming interface to define ML antiquotations -- NB: the transformed context ignores updates of the context parser; added command 'print_ML_antiquotations';
2014-03-06 wenzelm 2014-03-06 merged
2014-03-06 wenzelm 2014-03-06 some NEWS;
2014-03-06 blanchet 2014-03-06 renamed 'fun_rel' to 'rel_fun'
2014-03-06 blanchet 2014-03-06 renamed 'prod_rel' to 'rel_prod'
2014-03-06 blanchet 2014-03-06 renamed 'sum_rel' to 'rel_sum'
2014-03-06 blanchet 2014-03-06 renamed 'filter_rel' to 'rel_filter'
2014-03-06 blanchet 2014-03-06 renamed 'vset_rel' to 'rel_vset'
2014-03-06 blanchet 2014-03-06 fixed NEWS
2014-03-06 blanchet 2014-03-06 renamed 'set_rel' to 'rel_set'
2014-03-06 blanchet 2014-03-06 renamed 'cset_rel' to 'rel_cset'
2014-03-06 blanchet 2014-03-06 renamed 'fset_rel' to 'rel_fset'
2014-03-06 blanchet 2014-03-06 renamed 'map_sum' to 'sum_map'
2014-03-03 blanchet 2014-03-03 tuned code
2014-03-03 blanchet 2014-03-03 updated NEWS
2014-03-03 blanchet 2014-03-03 rationalized internals
2014-03-01 haftmann 2014-03-01 more precise imports; avoid duplicated simp rules in fact collections; dropped redundancy
2014-02-26 haftmann 2014-02-26 prefer proof context over background theory
2014-02-24 wenzelm 2014-02-24 tuned;
2014-02-23 haftmann 2014-02-23 NEWS and documentation, including correction of long-overseen "*"
2014-02-23 haftmann 2014-02-23 dropped long-unused option
2014-02-22 wenzelm 2014-02-22 NEWS;
2014-02-21 wenzelm 2014-02-21 improved completion based on context information;
2014-02-21 blanchet 2014-02-21 NEWS
2014-02-20 wenzelm 2014-02-20 clarified markup cumulation order (see also 25306d92f4ad and 0009a6ebc83b), e.g. relevant for completion_context;
2014-02-19 blanchet 2014-02-19 updated NEWS
2014-02-19 traytel 2014-02-19 reflect 207538943038 in NEWS
2014-02-17 wenzelm 2014-02-17 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 wenzelm 2014-02-17 NEWS;
2014-02-17 blanchet 2014-02-17 updated NEWS
2014-02-16 blanchet 2014-02-16 folded 'rel_option' into 'option_rel'
2014-02-16 blanchet 2014-02-16 folded 'list_all2' with the relator generated by 'datatype_new'
2014-02-16 blanchet 2014-02-16 more NEWS
2014-02-12 blanchet 2014-02-12 [mq]: news
2014-02-10 wenzelm 2014-02-10 discontinued axiomatic 'classes', 'classrel', 'arities';
2014-02-04 Lars Hupel 2014-02-04 interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
2014-02-04 blanchet 2014-02-04 removed legacy 'metisFT' method
2014-02-03 blanchet 2014-02-03 renamed 'smt' option 'smt_proofs' to avoid clash with 'smt' prover
2014-02-03 blanchet 2014-02-03 added new option to documentation
2014-01-30 blanchet 2014-01-30 renamed Sledgehammer options for symmetry between positive and negative versions
2014-01-26 wenzelm 2014-01-26 discontinued obsolete attribute "standard";
2014-01-25 wenzelm 2014-01-25 explicit eigen-context for attributes "where", "of", and corresponding read_instantiate, instantiate_tac;
2014-01-25 wenzelm 2014-01-25 NEWS for 31afce809794;
2014-01-22 wenzelm 2014-01-22 NEWS;
2014-01-22 wenzelm 2014-01-22 merged
2014-01-22 wenzelm 2014-01-22 inner syntax token language allows regular quoted strings; tuned signature;
2014-01-21 blanchet 2014-01-21 updated NEWS
2014-01-19 boehmes 2014-01-19 removed obsolete remote_cvc3 and remote_z3
2014-01-17 wenzelm 2014-01-17 clarified @{rail} syntax: prefer explicit \<newline> symbol;
2014-01-15 wenzelm 2014-01-15 added \<newline> symbol, which is used for char/string literals in HOL;
2014-01-13 wenzelm 2014-01-13 activation of Z3 via "z3_non_commercial" system option (without requiring restart);
2014-01-13 wenzelm 2014-01-13 tuned;