Thu, 04 Nov 2010 10:58:03 +0100 wenzelm clarified tooltips: message output by default, extra info via control/command;
Thu, 04 Nov 2010 10:33:37 +0100 wenzelm warn in correlation with report -- avoid spurious message duplicates;
Thu, 04 Nov 2010 10:22:59 +0100 wenzelm tuned;
Wed, 03 Nov 2010 21:53:56 +0100 wenzelm feeder: treat header as escaped utf8 to allow initial ML text to refer to non-ASCII file/directory names (e.g. "Documents/" on Chinese Ubuntu);
Wed, 03 Nov 2010 17:11:40 +0100 boehmes merged
Wed, 03 Nov 2010 17:02:53 +0100 boehmes updated SMT certificates
Wed, 03 Nov 2010 16:44:38 +0100 boehmes standardize timeout value based on reals
Wed, 03 Nov 2010 15:56:15 +0100 wenzelm merged
Wed, 03 Nov 2010 07:02:09 -0700 huffman merged
Sat, 30 Oct 2010 15:13:11 -0700 huffman change default_sort of HOLCF from pcpo to bifinite; rename command 'new_domain' to 'domain'; rename 'domain' to 'domain (unsafe)'
Sat, 30 Oct 2010 12:25:18 -0700 huffman merged
Fri, 29 Oct 2010 17:15:28 -0700 huffman renamed {Rep,Abs}_CFun to {Rep,Abs}_cfun
Fri, 29 Oct 2010 16:51:40 -0700 huffman renamed lemma cont2cont_Rep_CFun to cont2cont_APP
Fri, 29 Oct 2010 16:24:07 -0700 huffman simplify proof of typedef_cont_Abs
Wed, 27 Oct 2010 15:50:01 -0700 huffman rename constant trifte to tr_case
Wed, 27 Oct 2010 14:31:39 -0700 huffman add 'LAM (Def x). t' as alternative syntax for 'FLIFT x. t'
Wed, 27 Oct 2010 14:15:54 -0700 huffman make syntax of continuous if-then-else consistent with HOL if-then-else
Wed, 27 Oct 2010 13:54:18 -0700 huffman rename lemmas *_defined_iff and *_strict_iff to *_bottom_iff
Wed, 03 Nov 2010 10:44:53 +0100 haftmann polyml_as_definition does not require explicit dependencies on external ML files
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
(0) -30000 -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip