NEWS
Thu, 13 May 2010 14:34:05 +0200 nipkow Multiset: renamed, added and tuned lemmas;
Wed, 12 May 2010 13:34:24 +0200 wenzelm minor tuning;
Wed, 12 May 2010 13:21:23 +0200 wenzelm reverted parts of 7902dc7ea11d -- note that NEWS of published Isabelle releases are essentially read-only;
Wed, 12 May 2010 11:13:33 +0200 hoelzl clarified NEWS entry
Wed, 12 May 2010 11:08:15 +0200 hoelzl merged
Wed, 12 May 2010 11:07:46 +0200 hoelzl added NEWS entry
Tue, 11 May 2010 12:05:19 -0700 huffman removed lemma real_sq_order; use power2_le_imp_le instead
Tue, 11 May 2010 11:58:34 -0700 huffman fix spelling of 'superseded'
Tue, 11 May 2010 11:57:14 -0700 huffman NEWS: removed theory PReal
Tue, 11 May 2010 11:40:39 -0700 huffman collected NEWS updates for HOLCF
Tue, 11 May 2010 08:36:02 +0200 haftmann 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
Tue, 11 May 2010 08:29:42 +0200 haftmann theorem Presburger.int_induct has been renamed to Int.int_bidirectional_induct
Thu, 06 May 2010 17:59:19 +0200 haftmann dropped duplicate comp_arith
Tue, 04 May 2010 14:44:30 +0200 wenzelm merged
Tue, 04 May 2010 08:55:34 +0200 haftmann NEWS
Mon, 03 May 2010 14:38:18 +0200 wenzelm old NEWS on global operations;
Thu, 29 Apr 2010 20:00:26 +0200 wenzelm removed some Emacs junk;
Thu, 29 Apr 2010 18:41:38 +0200 haftmann merged
Thu, 29 Apr 2010 15:00:39 +0200 haftmann NEWS: code_reflect
Thu, 29 Apr 2010 17:47:53 +0200 wenzelm allow concrete syntax for local entities within a proof body, either via regular mixfix annotations to 'fix' etc. or the separate 'write' command;
Wed, 28 Apr 2010 13:29:57 +0200 haftmann merged
Wed, 28 Apr 2010 13:29:39 +0200 haftmann empty class specifcations observe default sort
Wed, 28 Apr 2010 12:21:55 +0200 wenzelm command 'defaultsort' is renamed to 'default_sort', it works within a local theory context;
Wed, 28 Apr 2010 08:25:02 +0200 haftmann term_typ: print styled term
Tue, 27 Apr 2010 21:46:10 +0200 wenzelm monotonic sort certification: sorts are no longer minimized at the kernel boundary, only when reading input from the end-user;
Tue, 27 Apr 2010 10:42:41 +0200 haftmann NEWS and CONTRIBUTORS
Mon, 26 Apr 2010 21:45:08 +0200 wenzelm command 'example_proof' opens an empty proof body;
Mon, 26 Apr 2010 11:34:15 +0200 haftmann dropped group_simps, ring_simps, field_eq_simps; classes division_ring_inverse_zero, field_inverse_zero, linordered_field_inverse_zero
Fri, 23 Apr 2010 22:48:07 +0200 wenzelm explicit 'schematic_theorem' etc. for schematic theorem statements;
Fri, 23 Apr 2010 13:58:14 +0200 haftmann modernized abstract algebra theories
Mon, 19 Apr 2010 10:56:26 +0200 wenzelm polyml-platform script is superseded by ISABELLE_PLATFORM;
Fri, 16 Apr 2010 22:18:59 +0200 wenzelm 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;
Fri, 16 Apr 2010 22:15:09 +0200 wenzelm separate commands 'hide_class', 'hide_type', 'hide_const', 'hide_fact';
Fri, 16 Apr 2010 10:52:10 +0200 wenzelm added ML antiquotation @{make_string}, which produces proper pretty printed version in Poly/ML 5.3.0 or later;
Thu, 15 Apr 2010 12:27:14 +0200 haftmann theory RBT with abstract type of red-black trees backed by implementation RBT_Impl
Wed, 07 Apr 2010 19:17:10 +0200 ballarin Merged resolving conflicts NEWS and locale.ML.
Mon, 15 Feb 2010 01:34:08 +0100 ballarin Graceful treatment of non-locale subgoals by methods unfold_locales and intro_locales.
Tue, 30 Mar 2010 23:12:55 +0200 krauss NEWS
Sun, 28 Mar 2010 16:13:29 +0200 wenzelm configuration options admit dynamic default values;
Sat, 27 Mar 2010 21:34:28 +0100 boehmes re-introduce reference to control simplifier tracing (needed for ProofGeneral settings menu) (cf. 12bb31230550)
Fri, 26 Mar 2010 23:46:22 +0100 boehmes replaced references 'trace_simp' and 'debug_simp' by configuration options stored in the context
Sat, 20 Mar 2010 17:33:11 +0100 wenzelm renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;
Wed, 17 Mar 2010 08:11:24 -0700 huffman NEWS: Nat_Bijection library
Sat, 13 Mar 2010 20:33:14 +0100 wenzelm local theory specifications handle hidden polymorphism implicitly;
Sat, 13 Mar 2010 17:19:12 +0100 wenzelm removed obsolete HOL/Library/Coinductive_List.thy, superceded by thys/Coinductive/Coinductive_List.thy in AFP/f2f5727b77d0;
Sat, 13 Mar 2010 15:12:47 +0100 wenzelm command 'typedef' now works within a local theory context;
Thu, 11 Mar 2010 15:52:33 +0100 haftmann NEWS
Thu, 11 Mar 2010 14:38:09 +0100 haftmann fixed typo
Tue, 09 Mar 2010 23:32:13 +0100 wenzelm localized typedecl;
Sat, 06 Mar 2010 15:39:16 +0100 wenzelm eliminated Args.bang_facts (legacy feature);
Wed, 03 Mar 2010 15:40:39 +0100 wenzelm authentic syntax for *all* logical entities;
Mon, 01 Mar 2010 17:09:42 +0100 wenzelm added type_notation command;
Sat, 27 Feb 2010 20:56:03 +0100 wenzelm clarified @{const_name} (only logical consts) vs. @{const_abbrev};
Sat, 27 Feb 2010 13:32:38 +0100 wenzelm ML antiquotations for type classes;
Fri, 26 Feb 2010 10:57:35 +0100 haftmann merged
Wed, 24 Feb 2010 14:34:40 +0100 haftmann renamed theory Rational to Rat
Thu, 25 Feb 2010 22:08:43 +0100 wenzelm more orthogonal antiquotations for type constructors;
Wed, 24 Feb 2010 20:37:01 +0100 wenzelm allow general mixfix syntax for type constructors;
Mon, 22 Feb 2010 16:03:48 +0100 haftmann NEWS
Mon, 22 Feb 2010 09:30:50 +0100 haftmann NEWS
less more (0) -1000 -300 -100 -60 tip