Fri, 19 Nov 2010 14:59:11 +0000 paulson merged
Fri, 19 Nov 2010 14:58:49 +0000 paulson First-order pattern matching: catch a rogue exception (differing numbers of arguments)
Fri, 19 Nov 2010 14:35:58 +0100 haftmann eval simp rules for predicate type, simplify primitive proofs
Fri, 19 Nov 2010 11:44:46 +0100 haftmann generalized type
Fri, 19 Nov 2010 10:37:06 +0100 haftmann made smlnj happy
Fri, 19 Nov 2010 10:04:08 +0100 haftmann merged
Thu, 18 Nov 2010 18:53:36 +0100 haftmann proper qualification needed due to shadowing on theory merge
Thu, 18 Nov 2010 17:06:02 +0100 haftmann more appropriate name for property
Thu, 18 Nov 2010 17:01:16 +0100 haftmann mapper for sum type
Thu, 18 Nov 2010 17:01:16 +0100 haftmann mapper for option type
Thu, 18 Nov 2010 17:01:16 +0100 haftmann mapper for list type; map_pair replaces prod_fun
Thu, 18 Nov 2010 17:01:16 +0100 haftmann map_pair replaces prod_fun
Thu, 18 Nov 2010 17:01:16 +0100 haftmann mapper for mulitset type
Thu, 18 Nov 2010 17:01:16 +0100 haftmann mapper for mapping type
Thu, 18 Nov 2010 17:01:15 +0100 haftmann mapper for fset type
Thu, 18 Nov 2010 17:01:15 +0100 haftmann mapper for dlist type
Thu, 18 Nov 2010 17:01:15 +0100 haftmann map_fun combinator in theory Fun
Thu, 18 Nov 2010 22:34:32 +0100 wenzelm some updates after 2 years of Mercurial usage;
Thu, 18 Nov 2010 18:12:03 +0100 blanchet mention Sledgehammer with SMT
Thu, 18 Nov 2010 18:09:08 +0100 blanchet enabled SMT solver in Sledgehammer by default
Thu, 18 Nov 2010 12:37:30 +0100 haftmann merged
Thu, 18 Nov 2010 10:59:42 +0100 haftmann keep variables bound
Thu, 18 Nov 2010 10:52:38 +0100 blanchet remove "Time limit reached" as potential error, because this is sometimes generated for individual slices and not for the entire problem
Wed, 17 Nov 2010 23:20:26 +0100 haftmann merged
Wed, 17 Nov 2010 17:27:25 +0100 haftmann infer variances of user-given mapper operation; proper thm storing
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
(0) -30000 -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip