Wed, 17 Nov 2010 21:35:23 +0100 nipkow code eqn for slice was missing; redefined splice with fun
Wed, 17 Nov 2010 08:47:58 -0800 huffman move strict function type into main HOLCF; instance cfun :: (predomain, domain) domain
Wed, 17 Nov 2010 06:49:23 -0800 huffman merged
Tue, 16 Nov 2010 16:36:57 -0800 huffman typedef (open) unit
Tue, 16 Nov 2010 13:37:17 -0800 huffman add bind_bind rules for powerdomains
Wed, 17 Nov 2010 13:50:02 +0100 wenzelm merged
Wed, 17 Nov 2010 12:24:58 +0100 haftmann emerging Isar command interface
Wed, 17 Nov 2010 11:38:47 +0100 haftmann fixed typo
Wed, 17 Nov 2010 11:38:46 +0100 haftmann updated keywords
Wed, 17 Nov 2010 11:27:48 +0100 haftmann ML signature interface
Wed, 17 Nov 2010 11:26:39 +0100 haftmann stub for Isar command interface
Wed, 17 Nov 2010 11:09:18 +0100 haftmann module for functorial mappers
Wed, 17 Nov 2010 13:39:30 +0100 wenzelm merged
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)
Wed, 17 Nov 2010 08:14:56 +0100 boehmes use the const antiquotation for constants (this checks that the constant is declared, whereas the more general term antiquotation treats undeclared names as free variable)
Wed, 17 Nov 2010 08:14:55 +0100 boehmes keep input and output files used to communicate with the SMT solver (for debugging purposes mainly)
Tue, 16 Nov 2010 12:08:28 -0800 huffman add lemmas about powerdomains
Tue, 16 Nov 2010 11:57:10 -0800 huffman declare {upper,lower,convex}_pd_induct as default induction rules
Tue, 16 Nov 2010 11:50:05 -0800 huffman rename 'repdef' to 'domaindef'
Wed, 17 Nov 2010 13:38:53 +0100 wenzelm refrain from opening Scratch.thy by default, to avoid bombing the editor with old/long theory text;
Wed, 17 Nov 2010 11:24:07 +0100 wenzelm less parentheses, cf. Session.welcome;
Tue, 16 Nov 2010 22:40:45 +0100 wenzelm avoid spam;
Tue, 16 Nov 2010 22:13:54 +0100 wenzelm more robust determination of java executable;
Tue, 16 Nov 2010 21:54:52 +0100 wenzelm init_component: require absolute path (when invoked by user scripts);
Tue, 16 Nov 2010 21:48:14 +0100 wenzelm more explicit explanation of init_component shell function;
Tue, 16 Nov 2010 20:30:25 +0100 wenzelm paranoia export of CLASSPATH, just in case the initial status via allexport is lost due to other scripts;
Tue, 16 Nov 2010 17:27:11 +0100 wenzelm tuned message;
Tue, 16 Nov 2010 15:29:01 +0100 wenzelm post raw messages last, to ensure that result has been handled by session actor already (e.g. to avoid race between Session.session_actor and Session_Dockable.main_actor);
Tue, 16 Nov 2010 15:23:26 +0100 wenzelm more reasonably defaults for typical laptops (2 GB RAM, 2 cores);
Tue, 16 Nov 2010 10:33:36 +0100 haftmann added forall2 predicate lifter
Mon, 15 Nov 2010 22:31:18 +0100 wenzelm merged
Mon, 15 Nov 2010 22:24:08 +0100 boehmes merged
Mon, 15 Nov 2010 22:23:28 +0100 boehmes renamed SMT failure: Abnormal_Termination is indeed more appropriate than Solver_Crashed
Mon, 15 Nov 2010 22:23:26 +0100 boehmes honour timeouts which are not rounded to full seconds
Mon, 15 Nov 2010 22:08:01 +0100 blanchet better error message
Mon, 15 Nov 2010 21:08:48 +0100 blanchet better error message
Mon, 15 Nov 2010 20:48:48 +0100 wenzelm merged
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;
(0) -30000 -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip