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
2010-11-05 wenzelm 2010-11-05 moved ISABELLE_IDENTIFIER from ISABELLE_OUTPUT further up to ISABELLE_HOME_USER;
2010-11-04 haftmann 2010-11-04 merged
2010-11-03 haftmann 2010-11-03 Theory Multiset provides stable quicksort implementation of sort_key.
2010-11-03 blanchet 2010-11-03 standardize on seconds for Nitpick and Sledgehammer timeouts
2010-11-03 wenzelm 2010-11-03 discontinued obsolete function sys_error and exception SYS_ERROR;
2010-10-31 nipkow 2010-10-31 merged
2010-10-29 nipkow 2010-10-29 Plus -> Sum_Type.Plus
2010-10-30 wenzelm 2010-10-30 support for real valued preferences;
2010-10-30 wenzelm 2010-10-30 support for real valued configuration options;
2010-10-29 wenzelm 2010-10-29 merged
2010-10-29 bulwahn 2010-10-29 NEWS
2010-10-28 wenzelm 2010-10-28 discontinued obsolete ML antiquotation @{theory_ref};
2010-10-26 krauss 2010-10-26 fixed typo
2010-10-26 krauss 2010-10-26 NEWS
2010-10-26 boehmes 2010-10-26 joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
2010-10-25 wenzelm 2010-10-25 merged
2010-10-25 wenzelm 2010-10-25 significantly improved Isabelle/Isar implementation manual;
2010-10-25 blanchet 2010-10-25 merged
2010-10-25 blanchet 2010-10-25 introduced manual version of "Auto Solve" as "solve_direct"
2010-10-25 wenzelm 2010-10-25 added ML antiquotation @{assert};