NEWS
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;
2010-03-13 wenzelm 2010-03-13 removed obsolete HOL/Library/Coinductive_List.thy, superceded by thys/Coinductive/Coinductive_List.thy in AFP/f2f5727b77d0;
2010-03-13 wenzelm 2010-03-13 command 'typedef' now works within a local theory context;
2010-03-11 haftmann 2010-03-11 NEWS
2010-03-11 haftmann 2010-03-11 fixed typo
2010-03-09 wenzelm 2010-03-09 localized typedecl;
2010-03-06 wenzelm 2010-03-06 eliminated Args.bang_facts (legacy feature);
2010-03-03 wenzelm 2010-03-03 authentic syntax for *all* logical entities;
2010-03-01 wenzelm 2010-03-01 added type_notation command;
2010-02-27 wenzelm 2010-02-27 clarified @{const_name} (only logical consts) vs. @{const_abbrev}; tuned;
2010-02-27 wenzelm 2010-02-27 ML antiquotations for type classes;
2010-02-26 haftmann 2010-02-26 merged
2010-02-24 haftmann 2010-02-24 renamed theory Rational to Rat
2010-02-25 wenzelm 2010-02-25 more orthogonal antiquotations for type constructors;
2010-02-24 wenzelm 2010-02-24 allow general mixfix syntax for type constructors;
2010-02-22 haftmann 2010-02-22 NEWS
2010-02-22 haftmann 2010-02-22 NEWS
2010-02-22 haftmann 2010-02-22 merged
2010-02-22 haftmann 2010-02-22 NEWS
2010-02-19 haftmann 2010-02-19 NEWS
2010-02-19 haftmann 2010-02-19 NEWS
2010-02-21 wenzelm 2010-02-21 tuned;
2010-02-21 wenzelm 2010-02-21 NEWS: authentic syntax for *all* term constants;
2010-02-15 wenzelm 2010-02-15 renamed InfixName to Infix etc.;
2010-02-15 wenzelm 2010-02-15 discontinued unnamed infix syntax;
2010-02-11 wenzelm 2010-02-11 added ML antiquotation @{syntax_const};
2010-02-10 wenzelm 2010-02-10 renamed Library/Quotient.thy to Library/Quotient_Type.thy to avoid clash with new theory Quotient in Main HOL;
2010-02-10 haftmann 2010-02-10 NEWS
2010-02-10 haftmann 2010-02-10 moved constants inverse and divide to Ring.thy
2010-02-08 haftmann 2010-02-08 renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
2010-02-08 haftmann 2010-02-08 NEWS: ax_simps
2010-02-08 haftmann 2010-02-08 merged
2010-02-08 haftmann 2010-02-08 separate library theory for type classes combining lattices with various algebraic structures
2010-02-08 haftmann 2010-02-08 merged
2010-02-08 haftmann 2010-02-08 separate theory for index structures
2010-02-05 haftmann 2010-02-05 more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
2010-02-07 wenzelm 2010-02-07 renamed old-style Drule.standard to Drule.export_without_context, to emphasize that this is in no way a standard operation;