NEWS
2010-05-27 wenzelm 2010-05-27 renamed structure PrintMode to Print_Mode, keeping the old name as legacy alias for some time;
2010-05-27 wenzelm 2010-05-27 renamed structure TypeInfer to Type_Infer, keeping the old name as legacy alias for some time;
2010-05-27 wenzelm 2010-05-27 misc updates for release;
2010-05-27 wenzelm 2010-05-27 constant Rat.normalize needs to be qualified;
2010-05-22 huffman 2010-05-22 NEWS: removed fixrec_simp attribute
2010-05-20 haftmann 2010-05-20 turned old-style mem into an input abbreviation
2010-05-18 huffman 2010-05-18 remove several redundant lemmas about floor and ceiling
2010-05-18 wenzelm 2010-05-18 merged
2010-05-17 haftmann 2010-05-17 dropped old Library/Word.thy and toy example ex/Adder.thy
2010-05-18 wenzelm 2010-05-18 do not open Legacy by default;
2010-05-17 wenzelm 2010-05-17 renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time; eliminated slightly odd alias structure T;
2010-05-15 wenzelm 2010-05-15 renamed structure OuterSyntax to Outer_Syntax, keeping the old name as alias for some time;
2010-05-15 wenzelm 2010-05-15 renamed structure SpecParse to Parse_Spec, keeping the old name as alias for some time;
2010-05-15 wenzelm 2010-05-15 renamed structure OuterKeyword to Keyword and OuterParse to Parse, keeping the old names as legacy aliases for some time;
2010-05-14 blanchet 2010-05-14 added some Sledgehammer news
2010-05-14 blanchet 2010-05-14 document Nitpick changes
2010-05-13 nipkow 2010-05-13 Multiset: renamed, added and tuned lemmas; Permutation: replaced local "remove" by List.remove1
2010-05-12 wenzelm 2010-05-12 minor tuning;
2010-05-12 wenzelm 2010-05-12 reverted parts of 7902dc7ea11d -- note that NEWS of published Isabelle releases are essentially read-only; (Spelling note: "supersede" is indeed more common in Isabelle sources, although "supercede" is also correct according to major dictionaries.)
2010-05-12 hoelzl 2010-05-12 clarified NEWS entry
2010-05-12 hoelzl 2010-05-12 merged
2010-05-12 hoelzl 2010-05-12 added NEWS entry
2010-05-11 huffman 2010-05-11 removed lemma real_sq_order; use power2_le_imp_le instead
2010-05-11 huffman 2010-05-11 fix spelling of 'superseded'
2010-05-11 huffman 2010-05-11 NEWS: removed theory PReal
2010-05-11 huffman 2010-05-11 collected NEWS updates for HOLCF
2010-05-11 haftmann 2010-05-11 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 haftmann 2010-05-11 theorem Presburger.int_induct has been renamed to Int.int_bidirectional_induct
2010-05-06 haftmann 2010-05-06 dropped duplicate comp_arith
2010-05-04 wenzelm 2010-05-04 merged
2010-05-04 haftmann 2010-05-04 NEWS
2010-05-03 wenzelm 2010-05-03 old NEWS on global operations;
2010-04-29 wenzelm 2010-04-29 removed some Emacs junk;
2010-04-29 haftmann 2010-04-29 merged
2010-04-29 haftmann 2010-04-29 NEWS: code_reflect
2010-04-29 wenzelm 2010-04-29 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 haftmann 2010-04-28 merged
2010-04-28 haftmann 2010-04-28 empty class specifcations observe default sort
2010-04-28 wenzelm 2010-04-28 command 'defaultsort' is renamed to 'default_sort', it works within a local theory context;
2010-04-28 haftmann 2010-04-28 term_typ: print styled term
2010-04-27 wenzelm 2010-04-27 monotonic sort certification: sorts are no longer minimized at the kernel boundary, only when reading input from the end-user;
2010-04-27 haftmann 2010-04-27 NEWS and CONTRIBUTORS
2010-04-26 wenzelm 2010-04-26 command 'example_proof' opens an empty proof body;
2010-04-26 haftmann 2010-04-26 dropped group_simps, ring_simps, field_eq_simps; classes division_ring_inverse_zero, field_inverse_zero, linordered_field_inverse_zero
2010-04-23 wenzelm 2010-04-23 explicit 'schematic_theorem' etc. for schematic theorem statements;
2010-04-23 haftmann 2010-04-23 modernized abstract algebra theories
2010-04-19 wenzelm 2010-04-19 polyml-platform script is superseded by ISABELLE_PLATFORM;
2010-04-16 wenzelm 2010-04-16 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 wenzelm 2010-04-16 separate commands 'hide_class', 'hide_type', 'hide_const', 'hide_fact';
2010-04-16 wenzelm 2010-04-16 added ML antiquotation @{make_string}, which produces proper pretty printed version in Poly/ML 5.3.0 or later;
2010-04-15 haftmann 2010-04-15 theory RBT with abstract type of red-black trees backed by implementation RBT_Impl
2010-04-07 ballarin 2010-04-07 Merged resolving conflicts NEWS and locale.ML.
2010-02-15 ballarin 2010-02-15 Graceful treatment of non-locale subgoals by methods unfold_locales and intro_locales.
2010-03-30 krauss 2010-03-30 NEWS
2010-03-28 wenzelm 2010-03-28 configuration options admit dynamic default values;
2010-03-27 boehmes 2010-03-27 re-introduce reference to control simplifier tracing (needed for ProofGeneral settings menu) (cf. 12bb31230550)
2010-03-26 boehmes 2010-03-26 replaced references 'trace_simp' and 'debug_simp' by configuration options stored in the context
2010-03-20 wenzelm 2010-03-20 renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;
2010-03-17 huffman 2010-03-17 NEWS: Nat_Bijection library
2010-03-13 wenzelm 2010-03-13 local theory specifications handle hidden polymorphism implicitly;