NEWS
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};
2010-10-24 nipkow 2010-10-24 renamed nat_number
2010-10-22 blanchet 2010-10-22 make Sledgehammer minimizer fully work with SMT
2010-10-21 blanchet 2010-10-21 use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
2010-10-14 krauss 2010-10-14 NEWS
2010-10-06 blanchet 2010-10-06 merged
2010-10-05 blanchet 2010-10-05 document latest changes to Meson/Metis/Sledgehammer
2010-10-04 haftmann 2010-10-04 turned distinct and sorted into inductive predicates: yields nice induction principles for free
2010-10-01 haftmann 2010-10-01 constant `contents` renamed to `the_elem`
2010-09-28 haftmann 2010-09-28 NEWS
2010-09-28 krauss 2010-09-28 no longer declare .psimps rules as [simp]. This regularly caused confusion (e.g., they show up in simp traces when the regular simp rules are disabled). In the few places where the rules are used, explicitly mentioning them actually clarifies the proof text.
2010-09-24 wenzelm 2010-09-24 clarified @{type} antiquotation: abbreviations and nonterminals count as "syntactic", disallow TFrees; tuned;
2010-09-23 haftmann 2010-09-23 CONTRIBUTORS and NEWS
2010-09-22 wenzelm 2010-09-22 renamed setmp_noncritical to Unsynchronized.setmp to emphasize its meaning;
2010-09-20 wenzelm 2010-09-20 renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
2010-09-17 wenzelm 2010-09-17 discontinued Output.debug, which belongs to early PGIP experiments (b6788dbd2ef9) and causes just too many problems (like spamming the message channel if it is used by more than one module);
2010-09-13 haftmann 2010-09-13 merged
2010-09-13 haftmann 2010-09-13 'class' and 'type' are now antiquoations by default
2010-09-13 nipkow 2010-09-13 renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
2010-09-13 nipkow 2010-09-13 added and renamed lemmas