Wed, 03 Nov 2010 13:54:23 +0100 wenzelm explicit warning about opaque signature matching -- saves extra paragraph in implementation manual;
Wed, 03 Nov 2010 11:33:51 +0100 wenzelm discontinued obsolete function sys_error and exception SYS_ERROR;
Wed, 03 Nov 2010 11:11:49 +0100 wenzelm replaced ancient sys_error by raise Fail, assuming that the latter is not handled specifically by the environment;
Wed, 03 Nov 2010 11:06:22 +0100 wenzelm replaced ancient sys_error by raise Fail, assuming that the latter is not handled specifically by the environment;
Wed, 03 Nov 2010 10:51:40 +0100 wenzelm try_param_tac: plain user error appears more appropriate;
Wed, 03 Nov 2010 10:48:55 +0100 wenzelm replaced ancient sys_error by raise Fail, assuming that the latter is not handled specifically by the environment;
Wed, 03 Nov 2010 10:20:37 +0100 wenzelm eliminated dead code;
Wed, 03 Nov 2010 10:18:05 +0100 wenzelm more conventional exceptions for abstract syntax operations -- eliminated ancient SYS_ERROR;
Wed, 03 Nov 2010 08:29:32 +0100 nipkow removed assumption
Tue, 02 Nov 2010 21:59:21 +0100 wenzelm more on naming tactics;
Tue, 02 Nov 2010 21:24:07 +0100 wenzelm merged
Tue, 02 Nov 2010 20:32:33 +0100 haftmann merged
Tue, 02 Nov 2010 16:59:40 +0100 haftmann tuned proof
Tue, 02 Nov 2010 16:48:19 +0100 haftmann tuned proof
Tue, 02 Nov 2010 16:36:33 +0100 haftmann tuned lemma proposition of properties_for_sort_key
Tue, 02 Nov 2010 16:31:57 +0100 haftmann lemmas sorted_map_same, sorted_same
Tue, 02 Nov 2010 16:31:56 +0100 haftmann lemmas multiset_of_filter, sort_key_by_quicksort
Tue, 02 Nov 2010 21:21:07 +0100 wenzelm more on "Time" in Isabelle/ML;
Tue, 02 Nov 2010 20:55:12 +0100 wenzelm simplified some time constants;
Tue, 02 Nov 2010 20:31:46 +0100 wenzelm added convenience operation seconds: real -> time;
Tue, 02 Nov 2010 20:16:56 +0100 wenzelm avoid catch-all exception handling;
Tue, 02 Nov 2010 20:15:57 +0100 wenzelm eliminated fragile catch-all pattern, based on educated guess about the intended exception;
Tue, 02 Nov 2010 12:37:12 +0100 traytel Attribute map_function -> coercion_map;
Sun, 31 Oct 2010 13:26:37 +0100 wenzelm syntax category "real" subsumes plain "int";
Sun, 31 Oct 2010 11:45:45 +0100 nipkow merged
Fri, 29 Oct 2010 17:57:36 +0200 nipkow Plus -> Sum_Type.Plus
Sun, 31 Oct 2010 11:38:09 +0100 ballarin Minor reformat.
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;
Sat, 30 Oct 2010 15:26:40 +0200 wenzelm support for floating-point tokens in outer syntax (coinciding with inner syntax version);
Fri, 29 Oct 2010 23:15:01 +0200 wenzelm merged
Fri, 29 Oct 2010 21:41:14 +0200 krauss added rule let_mono
Fri, 29 Oct 2010 22:59:40 +0200 wenzelm CONTRIBUTORS;
Fri, 29 Oct 2010 22:54:54 +0200 wenzelm more sharing of operations, without aliases;
Fri, 29 Oct 2010 22:22:36 +0200 wenzelm simplified data lookup;
Fri, 29 Oct 2010 22:19:27 +0200 wenzelm export declarations by default, to allow other ML packages by-pass concrete syntax;
Fri, 29 Oct 2010 22:07:48 +0200 wenzelm proper signature constraint for ML structure;
Fri, 29 Oct 2010 21:49:33 +0200 wenzelm proper header;
Fri, 29 Oct 2010 21:34:07 +0200 wenzelm Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
Fri, 29 Oct 2010 18:17:11 +0200 boehmes updated SMT certificates
Fri, 29 Oct 2010 18:17:10 +0200 boehmes eta-expand built-in constants; also rewrite partially applied natural number terms
Fri, 29 Oct 2010 18:17:09 +0200 boehmes optionally drop assumptions which cannot be preprocessed
Fri, 29 Oct 2010 18:17:08 +0200 boehmes added crafted list of SMT built-in constants
Fri, 29 Oct 2010 18:17:06 +0200 boehmes clarified error message
Fri, 29 Oct 2010 18:17:05 +0200 boehmes tuned
Fri, 29 Oct 2010 18:17:04 +0200 boehmes introduced SMT.distinct as a representation of the solvers' built-in predicate; check that SMT.distinct is always applied to an explicit list
Fri, 29 Oct 2010 17:38:57 +0200 wenzelm merged
Fri, 29 Oct 2010 17:28:27 +0200 nipkow added listrel1
Fri, 29 Oct 2010 17:25:22 +0200 nipkow hide Sum_Type.Plus
Fri, 29 Oct 2010 16:51:20 +0200 wenzelm merged
Fri, 29 Oct 2010 16:04:35 +0200 haftmann added user aliasses (still unclear how to specify names with whitespace contained)
Fri, 29 Oct 2010 14:06:10 +0200 haftmann merged
Fri, 29 Oct 2010 14:03:02 +0200 haftmann tuned structure of theory
Fri, 29 Oct 2010 13:49:49 +0200 haftmann remove term_of equations for Heap type explicitly
Fri, 29 Oct 2010 12:49:05 +0200 blanchet no need for setting up the kodkodi environment since Kodkodi 1.2.9
Fri, 29 Oct 2010 12:49:05 +0200 blanchet fixed order of quantifier instantiation in new Skolemizer
Fri, 29 Oct 2010 12:49:05 +0200 blanchet restructure Skolemization code slightly
Fri, 29 Oct 2010 12:49:05 +0200 blanchet ensure that MESON correctly preserves the name of variables (needed by the new Skolemizer)
Fri, 29 Oct 2010 12:49:05 +0200 blanchet more work on new Skolemizer without Hilbert_Choice
Fri, 29 Oct 2010 12:49:05 +0200 blanchet fix cluster numbering in the absense of Hilbert_Choice (reverts acde1b606b0e, effectively reintroducing most of 0bfaaa81fc62)
(0) -30000 -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip