Mon, 15 Nov 2010 18:58:30 +0100 blanchet cosmetics
Mon, 15 Nov 2010 18:56:31 +0100 blanchet interpret SMT_Failure.Solver_Crashed correctly
Mon, 15 Nov 2010 18:56:30 +0100 blanchet turn on Sledgehammer verbosity so we can track down crashes
Mon, 15 Nov 2010 18:56:29 +0100 blanchet pick up SMT solver crashes and report them to the user/Mirabelle if desired
Mon, 15 Nov 2010 18:04:04 +0100 boehmes merged
Mon, 15 Nov 2010 17:52:48 +0100 boehmes only replace unknowns of type nat with known integer numbers, don't alias unknown values in Z3's counterexamples with known integers
Mon, 15 Nov 2010 17:35:57 +0100 boehmes trace more solver output before raising an exception due to a non-zero return code (avoids truncating potential counterexamples produced by Z3)
Mon, 15 Nov 2010 17:04:53 +0100 bulwahn merged
Mon, 15 Nov 2010 13:40:12 +0100 bulwahn ignoring the constant STR in the predicate compiler
Mon, 15 Nov 2010 17:40:38 +0100 wenzelm non-executable source files;
Mon, 15 Nov 2010 17:39:23 +0100 wenzelm eliminated old-style sed in favour of builtin regex matching;
Mon, 15 Nov 2010 17:14:43 +0100 wenzelm more robust treatment of spaces in file names;
Mon, 15 Nov 2010 15:41:58 +0100 wenzelm tuned error messages;
Mon, 15 Nov 2010 14:59:53 +0100 wenzelm merged
Mon, 15 Nov 2010 14:59:21 +0100 haftmann re-generalized type of option_rel and sum_rel (accident from 2989f9f3aa10)
Mon, 15 Nov 2010 14:14:38 +0100 haftmann re-generalized type of prod_rel (accident from 2989f9f3aa10)
Mon, 15 Nov 2010 00:20:36 +0100 boehmes formal dependency on b2i files
Sun, 14 Nov 2010 23:55:25 +0100 boehmes merged
Fri, 12 Nov 2010 17:28:43 +0100 boehmes check the return code of the SMT solver and raise an exception if the prover failed
Sun, 14 Nov 2010 17:33:28 +0100 wenzelm updated README;
Sun, 14 Nov 2010 15:25:01 +0100 wenzelm tuned;
Sun, 14 Nov 2010 15:21:49 +0100 wenzelm cover 'write' as primitive proof command;
Sun, 14 Nov 2010 14:05:08 +0100 wenzelm clarified interact/print state: proof commands are treated as in TTY mode to get full response;
Sat, 13 Nov 2010 22:33:07 +0100 wenzelm somewhat adhoc replacement for 'thus' and 'hence';
Sat, 13 Nov 2010 21:46:24 +0100 wenzelm always print state of proof commands (notably "qed" etc.);
Sat, 13 Nov 2010 21:01:03 +0100 wenzelm simplified message: malformed symbols are fully internalized, i.e. can be printed without crashing;
Sat, 13 Nov 2010 20:49:02 +0100 wenzelm tuned message;
Sat, 13 Nov 2010 20:20:05 +0100 wenzelm proper escape in regex;
Sat, 13 Nov 2010 20:13:35 +0100 wenzelm report malformed symbols;
Sat, 13 Nov 2010 20:06:52 +0100 wenzelm qualified Symbol_Pos.symbol;
Sat, 13 Nov 2010 19:55:45 +0100 wenzelm total Symbol.source;
Sat, 13 Nov 2010 19:47:23 +0100 wenzelm eliminated slightly odd pervasive Symbol_Pos.symbol;
Sat, 13 Nov 2010 19:27:41 +0100 wenzelm treat Unicode "replacement character" (i.e. decoding error) is malformed;
Sat, 13 Nov 2010 19:21:53 +0100 wenzelm simplified/robustified treatment of malformed symbols, which are now fully internalized (total Symbol.explode etc.);
Sat, 13 Nov 2010 16:46:00 +0100 wenzelm tuned;
Sat, 13 Nov 2010 12:32:21 +0100 wenzelm back to quick_and_dirty, which is still practically important since the scheduler does not jump over subproofs;
Sat, 13 Nov 2010 11:41:02 +0100 wenzelm await_cancellation in the main thread, independently of the execution futures, which might get interrupted or be absent after node deletetion;
Sat, 13 Nov 2010 00:24:41 +0100 wenzelm updated README;
Fri, 12 Nov 2010 21:37:01 +0100 wenzelm defensive defaults for more robust experience for new users;
Fri, 12 Nov 2010 17:44:03 +0100 wenzelm merged
Fri, 12 Nov 2010 15:56:11 +0100 boehmes preliminary support for newer versions of Z3
Fri, 12 Nov 2010 15:56:10 +0100 boehmes turned SMT counterexamples into verbose messages (they had been swallowed before, following the state of smt_trace -- which is off by default), because they might be useful for the user
Fri, 12 Nov 2010 15:56:08 +0100 boehmes let the theory formally depend on the Boogie output
Fri, 12 Nov 2010 15:56:07 +0100 boehmes look for certificates relative to the theory
Fri, 12 Nov 2010 15:56:06 +0100 boehmes dropped numerals from monomorphization blacklist (only particular numerals are builtin, all other numerals should be treated uninterpreted), this blacklist should contain only truely polymorphic builtin constants supported by SMT
Fri, 12 Nov 2010 06:11:29 -0800 huffman merged
Fri, 12 Nov 2010 06:05:26 -0800 huffman update Theory.requires with new theory name
Fri, 12 Nov 2010 14:51:28 +0100 wenzelm tuned signatures;
Fri, 12 Nov 2010 14:06:37 +0100 wenzelm never open Unsynchronized;
Fri, 12 Nov 2010 12:57:02 +0100 wenzelm merged
Wed, 10 Nov 2010 18:45:48 -0800 huffman section headings
Wed, 10 Nov 2010 18:37:11 -0800 huffman reorder chapters for generated document
Wed, 10 Nov 2010 18:30:17 -0800 huffman merge Representable.thy into Domain.thy
Wed, 10 Nov 2010 18:15:21 -0800 huffman move stuff from Domain.thy to Domain_Aux.thy
Wed, 10 Nov 2010 17:56:08 -0800 huffman move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
Wed, 10 Nov 2010 14:59:52 -0800 huffman allow unpointed lazy arguments for definitional domain package
Wed, 10 Nov 2010 14:20:47 -0800 huffman add lemmas lub_below, below_lub; simplify some proofs; remove some unused lemmas
Wed, 10 Nov 2010 13:22:39 -0800 huffman merged
Wed, 10 Nov 2010 13:08:42 -0800 huffman removed unused lemma chain_mono2
Wed, 10 Nov 2010 11:42:35 -0800 huffman rename class 'bifinite' to 'domain'
(0) -30000 -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip