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
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;