haftmann [Wed, 03 Nov 2010 12:20:33 +0100] rev 40349
moved theory Quicksort from Library/ to ex/
haftmann [Wed, 03 Nov 2010 12:20:33 +0100] rev 40348
Theory Multiset provides stable quicksort implementation of sort_key.
haftmann [Wed, 03 Nov 2010 12:15:47 +0100] rev 40347
added code lemmas for stable parametrized quicksort
haftmann [Wed, 03 Nov 2010 11:50:29 +0100] rev 40346
tuned proof
blanchet [Thu, 04 Nov 2010 09:53:23 +0100] rev 40345
moved file in makefile to reflect actual dependencies
blanchet [Wed, 03 Nov 2010 23:01:30 +0100] rev 40344
give E one more second, to prevent cases where it finds a proof but has no time to print it
blanchet [Wed, 03 Nov 2010 22:51:32 +0100] rev 40343
use floating-point numbers for Sledgehammer's "thresholds" option rather than percentages;
updated docs
blanchet [Wed, 03 Nov 2010 22:33:23 +0100] rev 40342
don't be overly verbose in Sledgehammer's minimizer
blanchet [Wed, 03 Nov 2010 22:26:53 +0100] rev 40341
standardize on seconds for Nitpick and Sledgehammer timeouts
nipkow [Wed, 03 Nov 2010 20:19:24 +0100] rev 40340
cleaned up
wenzelm [Thu, 04 Nov 2010 16:15:13 +0100] rev 40339
added property "tooltip-margin";
wenzelm [Thu, 04 Nov 2010 10:58:03 +0100] rev 40338
clarified tooltips: message output by default, extra info via control/command;
wenzelm [Thu, 04 Nov 2010 10:33:37 +0100] rev 40337
warn in correlation with report -- avoid spurious message duplicates;
wenzelm [Thu, 04 Nov 2010 10:22:59 +0100] rev 40336
tuned;
wenzelm [Wed, 03 Nov 2010 21:53:56 +0100] rev 40335
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);
boehmes [Wed, 03 Nov 2010 17:11:40 +0100] rev 40334
merged
boehmes [Wed, 03 Nov 2010 17:02:53 +0100] rev 40333
updated SMT certificates
boehmes [Wed, 03 Nov 2010 16:44:38 +0100] rev 40332
standardize timeout value based on reals
wenzelm [Wed, 03 Nov 2010 15:56:15 +0100] rev 40331
merged
huffman [Wed, 03 Nov 2010 07:02:09 -0700] rev 40330
merged
huffman [Sat, 30 Oct 2010 15:13:11 -0700] rev 40329
change default_sort of HOLCF from pcpo to bifinite; rename command 'new_domain' to 'domain'; rename 'domain' to 'domain (unsafe)'
huffman [Sat, 30 Oct 2010 12:25:18 -0700] rev 40328
merged
huffman [Fri, 29 Oct 2010 17:15:28 -0700] rev 40327
renamed {Rep,Abs}_CFun to {Rep,Abs}_cfun
huffman [Fri, 29 Oct 2010 16:51:40 -0700] rev 40326
renamed lemma cont2cont_Rep_CFun to cont2cont_APP
huffman [Fri, 29 Oct 2010 16:24:07 -0700] rev 40325
simplify proof of typedef_cont_Abs
huffman [Wed, 27 Oct 2010 15:50:01 -0700] rev 40324
rename constant trifte to tr_case
huffman [Wed, 27 Oct 2010 14:31:39 -0700] rev 40323
add 'LAM (Def x). t' as alternative syntax for 'FLIFT x. t'
huffman [Wed, 27 Oct 2010 14:15:54 -0700] rev 40322
make syntax of continuous if-then-else consistent with HOL if-then-else
huffman [Wed, 27 Oct 2010 13:54:18 -0700] rev 40321
rename lemmas *_defined_iff and *_strict_iff to *_bottom_iff
haftmann [Wed, 03 Nov 2010 10:44:53 +0100] rev 40320
polyml_as_definition does not require explicit dependencies on external ML files
wenzelm [Wed, 03 Nov 2010 13:54:23 +0100] rev 40319
explicit warning about opaque signature matching -- saves extra paragraph in implementation manual;
wenzelm [Wed, 03 Nov 2010 11:33:51 +0100] rev 40318
discontinued obsolete function sys_error and exception SYS_ERROR;
wenzelm [Wed, 03 Nov 2010 11:11:49 +0100] rev 40317
replaced ancient sys_error by raise Fail, assuming that the latter is not handled specifically by the environment;
wenzelm [Wed, 03 Nov 2010 11:06:22 +0100] rev 40316
replaced ancient sys_error by raise Fail, assuming that the latter is not handled specifically by the environment;
wenzelm [Wed, 03 Nov 2010 10:51:40 +0100] rev 40315
try_param_tac: plain user error appears more appropriate;
wenzelm [Wed, 03 Nov 2010 10:48:55 +0100] rev 40314
replaced ancient sys_error by raise Fail, assuming that the latter is not handled specifically by the environment;
wenzelm [Wed, 03 Nov 2010 10:20:37 +0100] rev 40313
eliminated dead code;
wenzelm [Wed, 03 Nov 2010 10:18:05 +0100] rev 40312
more conventional exceptions for abstract syntax operations -- eliminated ancient SYS_ERROR;
proper signature constraint;
nipkow [Wed, 03 Nov 2010 08:29:32 +0100] rev 40311
removed assumption
wenzelm [Tue, 02 Nov 2010 21:59:21 +0100] rev 40310
more on naming tactics;
wenzelm [Tue, 02 Nov 2010 21:24:07 +0100] rev 40309
merged
haftmann [Tue, 02 Nov 2010 20:32:33 +0100] rev 40308
merged
haftmann [Tue, 02 Nov 2010 16:59:40 +0100] rev 40307
tuned proof
haftmann [Tue, 02 Nov 2010 16:48:19 +0100] rev 40306
tuned proof
haftmann [Tue, 02 Nov 2010 16:36:33 +0100] rev 40305
tuned lemma proposition of properties_for_sort_key
haftmann [Tue, 02 Nov 2010 16:31:57 +0100] rev 40304
lemmas sorted_map_same, sorted_same
haftmann [Tue, 02 Nov 2010 16:31:56 +0100] rev 40303
lemmas multiset_of_filter, sort_key_by_quicksort
wenzelm [Tue, 02 Nov 2010 21:21:07 +0100] rev 40302
more on "Time" in Isabelle/ML;
wenzelm [Tue, 02 Nov 2010 20:55:12 +0100] rev 40301
simplified some time constants;
wenzelm [Tue, 02 Nov 2010 20:31:46 +0100] rev 40300
added convenience operation seconds: real -> time;
wenzelm [Tue, 02 Nov 2010 20:16:56 +0100] rev 40299
avoid catch-all exception handling;
wenzelm [Tue, 02 Nov 2010 20:15:57 +0100] rev 40298
eliminated fragile catch-all pattern, based on educated guess about the intended exception;
traytel [Tue, 02 Nov 2010 12:37:12 +0100] rev 40297
Attribute map_function -> coercion_map;
tuned;
wenzelm [Sun, 31 Oct 2010 13:26:37 +0100] rev 40296
syntax category "real" subsumes plain "int";
nipkow [Sun, 31 Oct 2010 11:45:45 +0100] rev 40295
merged
nipkow [Fri, 29 Oct 2010 17:57:36 +0200] rev 40294
Plus -> Sum_Type.Plus
ballarin [Sun, 31 Oct 2010 11:38:09 +0100] rev 40293
Minor reformat.
wenzelm [Sat, 30 Oct 2010 21:08:20 +0200] rev 40292
support for real valued preferences;
wenzelm [Sat, 30 Oct 2010 16:33:58 +0200] rev 40291
support for real valued configuration options;
wenzelm [Sat, 30 Oct 2010 15:26:40 +0200] rev 40290
support for floating-point tokens in outer syntax (coinciding with inner syntax version);
wenzelm [Fri, 29 Oct 2010 23:15:01 +0200] rev 40289
merged
krauss [Fri, 29 Oct 2010 21:41:14 +0200] rev 40288
added rule let_mono
wenzelm [Fri, 29 Oct 2010 22:59:40 +0200] rev 40287
CONTRIBUTORS;
wenzelm [Fri, 29 Oct 2010 22:54:54 +0200] rev 40286
more sharing of operations, without aliases;
wenzelm [Fri, 29 Oct 2010 22:22:36 +0200] rev 40285
simplified data lookup;
wenzelm [Fri, 29 Oct 2010 22:19:27 +0200] rev 40284
export declarations by default, to allow other ML packages by-pass concrete syntax;
proper Args parsing for attribute syntax (required for proper treatment of morphisms when declarations are moved between contexts);
tuned;
wenzelm [Fri, 29 Oct 2010 22:07:48 +0200] rev 40283
proper signature constraint for ML structure;
explicit theory setup, which is customary outside Pure;
formal @{binding} instead of Binding.name;
wenzelm [Fri, 29 Oct 2010 21:49:33 +0200] rev 40282
proper header;
tuned whitespace;
wenzelm [Fri, 29 Oct 2010 21:34:07 +0200] rev 40281
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
boehmes [Fri, 29 Oct 2010 18:17:11 +0200] rev 40280
updated SMT certificates
boehmes [Fri, 29 Oct 2010 18:17:10 +0200] rev 40279
eta-expand built-in constants; also rewrite partially applied natural number terms
boehmes [Fri, 29 Oct 2010 18:17:09 +0200] rev 40278
optionally drop assumptions which cannot be preprocessed
boehmes [Fri, 29 Oct 2010 18:17:08 +0200] rev 40277
added crafted list of SMT built-in constants
boehmes [Fri, 29 Oct 2010 18:17:06 +0200] rev 40276
clarified error message
boehmes [Fri, 29 Oct 2010 18:17:05 +0200] rev 40275
tuned
boehmes [Fri, 29 Oct 2010 18:17:04 +0200] rev 40274
introduced SMT.distinct as a representation of the solvers' built-in predicate; check that SMT.distinct is always applied to an explicit list
wenzelm [Fri, 29 Oct 2010 17:38:57 +0200] rev 40273
merged
nipkow [Fri, 29 Oct 2010 17:28:27 +0200] rev 40272
added listrel1
nipkow [Fri, 29 Oct 2010 17:25:22 +0200] rev 40271
hide Sum_Type.Plus
wenzelm [Fri, 29 Oct 2010 16:51:20 +0200] rev 40270
merged
haftmann [Fri, 29 Oct 2010 16:04:35 +0200] rev 40269
added user aliasses (still unclear how to specify names with whitespace contained)
haftmann [Fri, 29 Oct 2010 14:06:10 +0200] rev 40268
merged
haftmann [Fri, 29 Oct 2010 14:03:02 +0200] rev 40267
tuned structure of theory
haftmann [Fri, 29 Oct 2010 13:49:49 +0200] rev 40266
remove term_of equations for Heap type explicitly
blanchet [Fri, 29 Oct 2010 12:49:05 +0200] rev 40265
no need for setting up the kodkodi environment since Kodkodi 1.2.9
blanchet [Fri, 29 Oct 2010 12:49:05 +0200] rev 40264
fixed order of quantifier instantiation in new Skolemizer
blanchet [Fri, 29 Oct 2010 12:49:05 +0200] rev 40263
restructure Skolemization code slightly
blanchet [Fri, 29 Oct 2010 12:49:05 +0200] rev 40262
ensure that MESON correctly preserves the name of variables (needed by the new Skolemizer)
blanchet [Fri, 29 Oct 2010 12:49:05 +0200] rev 40261
more work on new Skolemizer without Hilbert_Choice
blanchet [Fri, 29 Oct 2010 12:49:05 +0200] rev 40260
fix cluster numbering in the absense of Hilbert_Choice (reverts acde1b606b0e, effectively reintroducing most of 0bfaaa81fc62)
blanchet [Fri, 29 Oct 2010 12:49:05 +0200] rev 40259
prevent type errors because of inconsistent skolem Var types by giving fresh indices to Skolems
blanchet [Fri, 29 Oct 2010 12:49:05 +0200] rev 40258
make handling of parameters more robust, by querying the goal
haftmann [Fri, 29 Oct 2010 11:35:28 +0200] rev 40257
actually pass "verbose" argument
wenzelm [Fri, 29 Oct 2010 16:16:10 +0200] rev 40256
eliminated obsolete \_ escape;
wenzelm [Fri, 29 Oct 2010 11:49:56 +0200] rev 40255
eliminated obsolete \_ escapes in rail environments;
wenzelm [Fri, 29 Oct 2010 11:35:47 +0200] rev 40254
proper markup of formal text;
wenzelm [Fri, 29 Oct 2010 11:07:21 +0200] rev 40253
merged
krauss [Fri, 29 Oct 2010 11:04:41 +0200] rev 40252
hide_const various constants, in particular to avoid ugly qualifiers in HOLCF
blanchet [Fri, 29 Oct 2010 10:40:36 +0200] rev 40251
reverted e31e3f0071d4 because "foo.bar(5)" (with quotes) is wrong
Lars Noschinski <noschinl@in.tum.de> [Fri, 29 Oct 2010 10:14:49 +0200] rev 40250
merged
Lars Noschinski <noschinl@in.tum.de> [Wed, 22 Sep 2010 09:56:39 +0200] rev 40249
Remove unnecessary premise of mult1_union
bulwahn [Fri, 29 Oct 2010 08:44:49 +0200] rev 40248
adapting HOL-Mutabelle to changes in quickcheck
bulwahn [Fri, 29 Oct 2010 08:44:46 +0200] rev 40247
NEWS
bulwahn [Fri, 29 Oct 2010 08:44:44 +0200] rev 40246
changed global fixed timeout to a configurable timeout for quickcheck; test parameters in quickcheck are now fully passed around with the context
bulwahn [Fri, 29 Oct 2010 08:44:43 +0200] rev 40245
updating documentation on quickcheck in the Isar reference
bulwahn [Thu, 28 Oct 2010 18:36:34 +0200] rev 40244
merged
bulwahn [Thu, 28 Oct 2010 17:28:45 +0200] rev 40243
adding a simple check to only run with a SWI-Prolog version known to work
* * *
taking the isabelle platform into account when finding the prolog system
wenzelm [Thu, 28 Oct 2010 23:54:39 +0200] rev 40242
tuned messages;
wenzelm [Thu, 28 Oct 2010 23:19:52 +0200] rev 40241
discontinued obsolete ML antiquotation @{theory_ref};
wenzelm [Thu, 28 Oct 2010 22:59:33 +0200] rev 40240
tuned;
wenzelm [Thu, 28 Oct 2010 22:39:59 +0200] rev 40239
moved FOL/ex/Iff_Oracle.thy to HOL/ex where it is more accessible to most readers of isar-ref;
tuned;
wenzelm [Thu, 28 Oct 2010 22:23:11 +0200] rev 40238
type attribute is derived concept outside the kernel;
wenzelm [Thu, 28 Oct 2010 22:12:08 +0200] rev 40237
preserve original source position of exn;
wenzelm [Thu, 28 Oct 2010 22:11:06 +0200] rev 40236
handle Type.TYPE_MATCH, not arbitrary exceptions via MATCH_TYPE variable;
clarified handle/raise wrt. Quotient_Info.NotFound -- avoid fragile unqualified NotFound depending on "open" scope;
added helpful comments;
wenzelm [Thu, 28 Oct 2010 22:04:00 +0200] rev 40235
use Exn.interruptible_capture to keep user-code interruptible (Exn.capture not immediately followed by Exn.release here);
wenzelm [Thu, 28 Oct 2010 21:59:01 +0200] rev 40234
added Exn.interruptible_capture, which reraises interrupts as required by user-code (when Exn.capture is not immediately followed by Exn.release);
refined Exn.is_interrupt: detect nested IO Interrupts;
generalized Exn.map_result;
more precise dependencies;
wenzelm [Thu, 28 Oct 2010 21:52:33 +0200] rev 40233
eliminated dead code;
wenzelm [Thu, 28 Oct 2010 21:51:34 +0200] rev 40232
tuned white-space;
nipkow [Thu, 28 Oct 2010 17:54:25 +0200] rev 40231
merged
nipkow [Thu, 28 Oct 2010 17:54:09 +0200] rev 40230
added lemmas about listrel(1)