2010-06-02 ago improved parallelism of proof term normalization;
2010-06-01 ago merged
2010-06-01 ago update NEWS
2010-06-01 ago removed "nitpick_intro" attribute -- Nitpick noew uses Spec_Rules instead
2010-06-01 ago added "atoms" option to Nitpick (request from Karlsruhe) + wrap Refute. functions to "nitpick_util.ML"
2010-05-31 ago notes on Isabelle/jEdit;
2010-05-31 ago modernized some structure names, keeping a few legacy aliases;
2010-05-27 ago merged
2010-05-27 ago merged
2010-05-27 ago moved SMT into the HOL image
2010-05-27 ago renamed structure PrintMode to Print_Mode, keeping the old name as legacy alias for some time;
2010-05-27 ago renamed structure TypeInfer to Type_Infer, keeping the old name as legacy alias for some time;
2010-05-27 ago misc updates for release;
2010-05-27 ago constant Rat.normalize needs to be qualified;
2010-05-22 ago NEWS: removed fixrec_simp attribute
2010-05-20 ago turned old-style mem into an input abbreviation
2010-05-18 ago remove several redundant lemmas about floor and ceiling
2010-05-18 ago merged
2010-05-17 ago dropped old Library/Word.thy and toy example ex/Adder.thy
2010-05-18 ago do not open Legacy by default;
2010-05-17 ago renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
2010-05-15 ago renamed structure OuterSyntax to Outer_Syntax, keeping the old name as alias for some time;
2010-05-15 ago renamed structure SpecParse to Parse_Spec, keeping the old name as alias for some time;
2010-05-15 ago renamed structure OuterKeyword to Keyword and OuterParse to Parse, keeping the old names as legacy aliases for some time;
2010-05-14 ago added some Sledgehammer news
2010-05-14 ago document Nitpick changes
2010-05-13 ago Multiset: renamed, added and tuned lemmas;
2010-05-12 ago minor tuning;
2010-05-12 ago reverted parts of 7902dc7ea11d -- note that NEWS of published Isabelle releases are essentially read-only;
2010-05-12 ago clarified NEWS entry
2010-05-12 ago merged
2010-05-12 ago added NEWS entry
2010-05-11 ago removed lemma real_sq_order; use power2_le_imp_le instead
2010-05-11 ago fix spelling of 'superseded'
2010-05-11 ago NEWS: removed theory PReal
2010-05-11 ago collected NEWS updates for HOLCF
2010-05-11 ago renamed former Int.int_induct to Int.int_of_nat_induct, former Presburger.int_induct to Int.int_induct: is more conservative and more natural than the intermediate solution
2010-05-11 ago theorem Presburger.int_induct has been renamed to Int.int_bidirectional_induct
2010-05-06 ago dropped duplicate comp_arith
2010-05-04 ago merged
2010-05-04 ago NEWS
2010-05-03 ago old NEWS on global operations;
2010-04-29 ago removed some Emacs junk;
2010-04-29 ago merged
2010-04-29 ago NEWS: code_reflect
2010-04-29 ago allow concrete syntax for local entities within a proof body, either via regular mixfix annotations to 'fix' etc. or the separate 'write' command;
2010-04-28 ago merged
2010-04-28 ago empty class specifcations observe default sort
2010-04-28 ago command 'defaultsort' is renamed to 'default_sort', it works within a local theory context;
2010-04-28 ago term_typ: print styled term
2010-04-27 ago monotonic sort certification: sorts are no longer minimized at the kernel boundary, only when reading input from the end-user;
2010-04-27 ago NEWS and CONTRIBUTORS
2010-04-26 ago command 'example_proof' opens an empty proof body;
2010-04-26 ago dropped group_simps, ring_simps, field_eq_simps; classes division_ring_inverse_zero, field_inverse_zero, linordered_field_inverse_zero
2010-04-23 ago explicit 'schematic_theorem' etc. for schematic theorem statements;
2010-04-23 ago modernized abstract algebra theories
2010-04-19 ago polyml-platform script is superseded by ISABELLE_PLATFORM;
2010-04-16 ago keep localized 'types' as regular non-old-style version -- 'type_abbrev' as 'type' just causes too many problems, e.g. clash with "type" in translations or "type:" argument syntax;
2010-04-16 ago separate commands 'hide_class', 'hide_type', 'hide_const', 'hide_fact';
2010-04-16 ago added ML antiquotation @{make_string}, which produces proper pretty printed version in Poly/ML 5.3.0 or later;