NEWS
Thu, 02 Dec 2010 08:34:23 +0100 nipkow coercions
Wed, 01 Dec 2010 19:33:49 +0100 hoelzl Updated NEWS
Wed, 01 Dec 2010 11:45:37 +0100 haftmann NEWS
Tue, 30 Nov 2010 15:58:21 +0100 haftmann merged
Mon, 29 Nov 2010 13:44:54 +0100 haftmann equivI has replaced equiv.intro
Mon, 29 Nov 2010 11:22:40 +0100 wenzelm added document antiquotation @{file};
Sun, 28 Nov 2010 13:58:29 +0100 wenzelm recovered Isabelle2009-2 NEWS -- published part is read-only;
Sat, 27 Nov 2010 13:12:10 -0800 huffman renamed several HOLCF theorems (listed in NEWS)
Fri, 26 Nov 2010 23:41:23 +0100 wenzelm merged
Fri, 26 Nov 2010 22:36:55 +0100 blanchet document changes in Nitpick and MESON/Metis
Fri, 26 Nov 2010 22:29:41 +0100 wenzelm make two copies (!) of Library.UnequalLengths coincide with ListPair.UnequalLengths;
Fri, 26 Nov 2010 14:19:16 +0100 wenzelm more correct spelling;
Fri, 26 Nov 2010 12:03:17 +0100 haftmann globbing constant expressions use more idiomatic underscore rather than star;
Mon, 22 Nov 2010 10:34:33 +0100 hoelzl Replace surj by abbreviation; remove surj_on.
Wed, 24 Nov 2010 10:23:52 +0100 bulwahn announcing some latest change (d40b347d5b0b)
Mon, 22 Nov 2010 17:49:12 +0100 haftmann merged
Mon, 22 Nov 2010 17:46:51 +0100 haftmann replaced misleading Fset/fset name -- these do not stand for finite sets
Mon, 22 Nov 2010 10:41:56 +0100 bulwahn renaming quickcheck generator code to random
Sat, 20 Nov 2010 00:53:26 +0100 wenzelm renamed raw "explode" function to "raw_explode" to emphasize its meaning;
Fri, 19 Nov 2010 09:07:23 -0800 huffman merged
Wed, 17 Nov 2010 12:19:19 -0800 huffman accumulated NEWS updates for HOLCF
Thu, 18 Nov 2010 18:12:03 +0100 blanchet mention Sledgehammer with SMT
Wed, 17 Nov 2010 09:22:23 +0100 boehmes require the b2i file ending in the boogie_open command (for consistency with the theory header)
Mon, 08 Nov 2010 12:13:44 +0100 boehmes 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)
Sat, 06 Nov 2010 00:10:32 +0100 krauss abolished obscure goal variant of [split_format] -- unused (cf. d1c14898fd04), unrelated to '(complete)' variant, and not at all canonical
Fri, 05 Nov 2010 23:19:20 +0100 wenzelm moved ISABELLE_IDENTIFIER from ISABELLE_OUTPUT further up to ISABELLE_HOME_USER;
Thu, 04 Nov 2010 09:54:16 +0100 haftmann merged
Wed, 03 Nov 2010 12:20:33 +0100 haftmann Theory Multiset provides stable quicksort implementation of sort_key.
Wed, 03 Nov 2010 22:26:53 +0100 blanchet standardize on seconds for Nitpick and Sledgehammer timeouts
Wed, 03 Nov 2010 11:33:51 +0100 wenzelm discontinued obsolete function sys_error and exception SYS_ERROR;
Sun, 31 Oct 2010 11:45:45 +0100 nipkow merged
Fri, 29 Oct 2010 17:57:36 +0200 nipkow Plus -> Sum_Type.Plus
Sat, 30 Oct 2010 21:08:20 +0200 wenzelm support for real valued preferences;
Sat, 30 Oct 2010 16:33:58 +0200 wenzelm support for real valued configuration options;
Fri, 29 Oct 2010 11:07:21 +0200 wenzelm merged
Fri, 29 Oct 2010 08:44:46 +0200 bulwahn NEWS
Thu, 28 Oct 2010 23:19:52 +0200 wenzelm discontinued obsolete ML antiquotation @{theory_ref};
Tue, 26 Oct 2010 15:06:36 +0200 krauss fixed typo
Tue, 26 Oct 2010 13:50:18 +0200 krauss NEWS
Tue, 26 Oct 2010 11:45:12 +0200 boehmes 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
Mon, 25 Oct 2010 16:18:00 +0200 wenzelm merged
Mon, 25 Oct 2010 16:17:16 +0200 wenzelm significantly improved Isabelle/Isar implementation manual;
Mon, 25 Oct 2010 11:42:05 +0200 blanchet merged
Mon, 25 Oct 2010 10:30:46 +0200 blanchet introduced manual version of "Auto Solve" as "solve_direct"
Mon, 25 Oct 2010 11:16:23 +0200 wenzelm added ML antiquotation @{assert};
Sun, 24 Oct 2010 20:37:30 +0200 nipkow renamed nat_number
Fri, 22 Oct 2010 11:11:34 +0200 blanchet make Sledgehammer minimizer fully work with SMT
Thu, 21 Oct 2010 14:55:09 +0200 blanchet use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
Thu, 14 Oct 2010 12:40:14 +0200 krauss NEWS
Wed, 06 Oct 2010 17:44:21 +0200 blanchet merged
Tue, 05 Oct 2010 12:06:08 +0200 blanchet document latest changes to Meson/Metis/Sledgehammer
Mon, 04 Oct 2010 14:46:48 +0200 haftmann turned distinct and sorted into inductive predicates: yields nice induction principles for free
Fri, 01 Oct 2010 16:05:25 +0200 haftmann constant `contents` renamed to `the_elem`
Tue, 28 Sep 2010 15:33:56 +0200 haftmann NEWS
Tue, 28 Sep 2010 09:54:07 +0200 krauss no longer declare .psimps rules as [simp].
Fri, 24 Sep 2010 16:17:59 +0200 wenzelm clarified @{type} antiquotation: abbreviations and nonterminals count as "syntactic", disallow TFrees;
Thu, 23 Sep 2010 09:53:52 +0200 haftmann CONTRIBUTORS and NEWS
Wed, 22 Sep 2010 18:21:48 +0200 wenzelm renamed setmp_noncritical to Unsynchronized.setmp to emphasize its meaning;
Mon, 20 Sep 2010 16:05:25 +0200 wenzelm renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
Fri, 17 Sep 2010 22:17:57 +0200 wenzelm 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);
less more (0) -1000 -300 -100 -60 tip