NEWS
2011-01-06 ballarin 2011-01-06 Documentation for 'interpret' and 'sublocale' with mixins.
2011-01-06 ballarin 2011-01-06 Abelian group facts obtained from group facts via interpretation (sublocale).
2011-01-06 boehmes 2011-01-06 differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3"); turned individual SMT solvers into components; made CVC3 the default SMT solver (Z3 is licensed as "non-commercial only"); tuned smt_filter interface
2011-01-04 huffman 2011-01-04 change some lemma names containing 'UU' to 'bottom'
2011-01-04 huffman 2011-01-04 renamed constant 'UU' to 'bottom', keeping 'UU' as alternative input syntax; removed redundant lemma UU_least
2010-12-29 wenzelm 2010-12-29 theory loader: implicit load path is considered legacy;
2010-12-23 huffman 2010-12-23 NEWS updates for HOLCF
2010-12-23 haftmann 2010-12-23 tuned order of NEWS
2010-12-23 haftmann 2010-12-23 NEWS
2010-12-21 wenzelm 2010-12-21 configuration option "rule_trace"; discontinued preference "trace-rules";
2010-12-21 wenzelm 2010-12-21 configuration option "syntax_ast_trace" and "syntax_ast_stat";
2010-12-20 wenzelm 2010-12-20 proper identifiers for consts and types;
2010-12-19 huffman 2010-12-19 rename function cprod_map to prod_map
2010-12-19 huffman 2010-12-19 fix typo
2010-12-19 huffman 2010-12-19 type 'defl' takes a type parameter again (cf. b525988432e9)
2010-12-19 huffman 2010-12-19 reintroduce 'bifinite' class, now with existentially-quantified approx function (cf. b525988432e9)
2010-12-17 wenzelm 2010-12-17 Command 'type_synonym' (with single argument) supersedes 'types' (legacy feature);
2010-12-17 wenzelm 2010-12-17 replaced command 'nonterminals' by slightly modernized version 'nonterminal';
2010-12-17 wenzelm 2010-12-17 renamed structure MetaSimplifier to raw_Simplifer, to emphasize its meaning;
2010-12-08 haftmann 2010-12-08 NEWS
2010-12-06 huffman 2010-12-06 merged
2010-12-06 huffman 2010-12-06 remove lemma cont_cfun; rename thelub_cfun to lub_cfun
2010-12-06 huffman 2010-12-06 rename lub_fun -> is_lub_fun, thelub_fun -> lub_fun
2010-12-03 hoelzl 2010-12-03 it is known as the extended reals, not the infinite reals
2010-12-06 wenzelm 2010-12-06 more correct NEWS;
2010-12-05 wenzelm 2010-12-05 IsabelleText font: include Cyrillic, Hebrew, Arabic from DejaVu Sans 2.32;
2010-12-05 wenzelm 2010-12-05 command 'notepad' replaces former 'example_proof';
2010-12-04 wenzelm 2010-12-04 added Syntax.default_root; simplified Syntax.parse operations; clarified treatment of syntax root for translation rules -- refrain from logical_type replacement; tuned error message;
2010-12-04 wenzelm 2010-12-04 added Syntax.pretty_priority;
2010-12-03 wenzelm 2010-12-03 minor tuning for release;
2010-12-03 wenzelm 2010-12-03 source files are always encoded as UTF-8;
2010-12-03 wenzelm 2010-12-03 setup subtyping/coercions once in HOL.thy, but enable it only later via configuration option;
2010-12-03 bulwahn 2010-12-03 NEWS
2010-12-02 wenzelm 2010-12-02 configuration option "show_abbrevs" supersedes print mode "no_abbrevs", with inverted meaning;
2010-12-02 wenzelm 2010-12-02 renamed trace_simp to simp_trace, and debug_simp to simp_debug;
2010-12-02 nipkow 2010-12-02 coercions
2010-12-01 hoelzl 2010-12-01 Updated NEWS
2010-12-01 haftmann 2010-12-01 NEWS
2010-11-30 haftmann 2010-11-30 merged
2010-11-29 haftmann 2010-11-29 equivI has replaced equiv.intro
2010-11-29 wenzelm 2010-11-29 added document antiquotation @{file};
2010-11-28 wenzelm 2010-11-28 recovered Isabelle2009-2 NEWS -- published part is read-only;
2010-11-27 huffman 2010-11-27 renamed several HOLCF theorems (listed in NEWS)
2010-11-26 wenzelm 2010-11-26 merged
2010-11-26 blanchet 2010-11-26 document changes in Nitpick and MESON/Metis
2010-11-26 wenzelm 2010-11-26 make two copies (!) of Library.UnequalLengths coincide with ListPair.UnequalLengths;
2010-11-26 wenzelm 2010-11-26 more correct spelling;
2010-11-26 haftmann 2010-11-26 globbing constant expressions use more idiomatic underscore rather than star; precised
2010-11-22 hoelzl 2010-11-22 Replace surj by abbreviation; remove surj_on.
2010-11-24 bulwahn 2010-11-24 announcing some latest change (d40b347d5b0b)
2010-11-22 haftmann 2010-11-22 merged
2010-11-22 haftmann 2010-11-22 replaced misleading Fset/fset name -- these do not stand for finite sets
2010-11-22 bulwahn 2010-11-22 renaming quickcheck generator code to random
2010-11-20 wenzelm 2010-11-20 renamed raw "explode" function to "raw_explode" to emphasize its meaning;
2010-11-19 huffman 2010-11-19 merged
2010-11-17 huffman 2010-11-17 accumulated NEWS updates for HOLCF
2010-11-18 blanchet 2010-11-18 mention Sledgehammer with SMT
2010-11-17 boehmes 2010-11-17 require the b2i file ending in the boogie_open command (for consistency with the theory header)
2010-11-08 boehmes 2010-11-08 better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
2010-11-06 krauss 2010-11-06 abolished obscure goal variant of [split_format] -- unused (cf. d1c14898fd04), unrelated to '(complete)' variant, and not at all canonical