Mon, 06 Dec 2010 13:34:05 -0800 huffman instance unit :: domain
Mon, 06 Dec 2010 12:53:06 -0800 huffman simplify ideal completion proofs
Mon, 06 Dec 2010 11:44:30 -0800 huffman remove unused lemmas
Mon, 06 Dec 2010 11:22:42 -0800 huffman remove lemma cont_cfun;
Mon, 06 Dec 2010 10:08:33 -0800 huffman rename lub_fun -> is_lub_fun, thelub_fun -> lub_fun
Mon, 06 Dec 2010 08:59:58 -0800 huffman pcpodef no longer generates _defined lemmas, use _bottom_iff lemmas instead
Mon, 06 Dec 2010 08:43:52 -0800 huffman cpodef no longer generates lemma is_lub_foo, since it is redundant with lub_foo
Mon, 06 Dec 2010 08:30:00 -0800 huffman add lemmas lub_APP, lub_LAM
Mon, 06 Dec 2010 19:54:56 +0100 hoelzl folding on arbitrary Lebesgue integrable functions
Mon, 06 Dec 2010 19:54:53 +0100 hoelzl fixed spelling errors
Mon, 06 Dec 2010 19:54:48 +0100 hoelzl move coercions to appropriate places
Fri, 03 Dec 2010 15:25:14 +0100 hoelzl it is known as the extended reals, not the infinite reals
Mon, 06 Dec 2010 19:18:02 +0100 nipkow moved coercion decl. for int
Mon, 06 Dec 2010 17:33:25 +0100 bulwahn adapting copied bash code in mutabelle script
Mon, 06 Dec 2010 16:37:15 +0100 wenzelm more correct NEWS;
Mon, 06 Dec 2010 16:18:56 +0100 wenzelm merged
Mon, 06 Dec 2010 13:46:45 +0100 blanchet fix monotonicity type of None
Mon, 06 Dec 2010 13:36:28 +0100 blanchet compile
Mon, 06 Dec 2010 13:33:09 +0100 blanchet introduced hack to exploit the symmetry of equality in monotonicity calculus
Mon, 06 Dec 2010 13:33:09 +0100 blanchet cleanup example
Mon, 06 Dec 2010 13:33:09 +0100 blanchet add more flexibility to the monotonicity calculus: instead of hardcoding F-arrows, also allow G-arrows, simulating applications of the Sub rule
Mon, 06 Dec 2010 13:33:09 +0100 blanchet fixed bug in monotonicity solution display, whereby the polarity of literals was ignored
Mon, 06 Dec 2010 13:33:09 +0100 blanchet improve precision of forall in constancy part of the monotonicity calculus
Mon, 06 Dec 2010 13:33:09 +0100 blanchet added some missing well-annotatedness constraints to monotonicity calculus
Mon, 06 Dec 2010 13:33:09 +0100 blanchet more work on the monotonicity evaluation driver
Mon, 06 Dec 2010 13:33:09 +0100 blanchet improve precision of finite functions in monotonicity calculus
Mon, 06 Dec 2010 13:33:09 +0100 blanchet added ML code for testing entire theories for monotonicity
Mon, 06 Dec 2010 13:33:09 +0100 blanchet use ML SAT solvers up to a certain time limit, then switch to faster solvers with a timeout -- this becomes necessary with the new, more powerful monotonicity calculus
Mon, 06 Dec 2010 13:33:09 +0100 blanchet added examples to exercise new monotonicity code
Mon, 06 Dec 2010 13:33:09 +0100 blanchet fixed quantifier handling of new monotonicity calculus
Mon, 06 Dec 2010 13:33:09 +0100 blanchet tune parentheses and indentation
Mon, 06 Dec 2010 13:33:09 +0100 blanchet proper handling of frames for connectives in monotonicity calculus
Mon, 06 Dec 2010 13:33:09 +0100 blanchet tune indentation
Mon, 06 Dec 2010 13:33:09 +0100 blanchet removed old baggage from monotonicity calculus -- the "calculus" option didn't really work anyway because of on-the-fly simplifications
Mon, 06 Dec 2010 13:33:05 +0100 blanchet implemented All rules from new monotonicity calculus
Mon, 06 Dec 2010 13:30:57 +0100 blanchet fixed bug in clause handling in monotonicity code, whereby the unsound rule False | x <--> False was used to simplify constraints
Mon, 06 Dec 2010 13:30:38 +0100 blanchet started implementing the new monotonicity rules for application
Mon, 06 Dec 2010 13:30:36 +0100 blanchet implemented connectives in new monotonicity calculus
Mon, 06 Dec 2010 13:29:23 +0100 blanchet added "Neq" operator to monotonicity inference module
Mon, 06 Dec 2010 13:26:27 +0100 blanchet started implementing connectives in new monotonicity calculus
Mon, 06 Dec 2010 13:26:23 +0100 blanchet more work on frames in the new monotonicity calculus
Mon, 06 Dec 2010 13:18:25 +0100 blanchet support 3 monotonicity calculi in one and fix soundness bug
Mon, 06 Dec 2010 13:18:25 +0100 blanchet tuning
Mon, 06 Dec 2010 13:18:25 +0100 blanchet proper handling of assignment disjunctions vs. conjunctions
Mon, 06 Dec 2010 13:18:25 +0100 blanchet adapt monotonicity code to four annotation types
Mon, 06 Dec 2010 13:18:25 +0100 blanchet more monotonicity tuning
Mon, 06 Dec 2010 13:18:25 +0100 blanchet tuning
Mon, 06 Dec 2010 13:18:25 +0100 blanchet added frame component to Gamma in monotonicity calculus
Mon, 06 Dec 2010 13:18:25 +0100 blanchet use boolean pair to encode annotation, which may now take four values
Mon, 06 Dec 2010 13:18:25 +0100 blanchet started generalizing monotonicity code to accommodate new calculus
Mon, 06 Dec 2010 13:17:26 +0100 blanchet merged
Mon, 06 Dec 2010 11:41:24 +0100 blanchet handle "max_relevant" uniformly
Mon, 06 Dec 2010 11:26:17 +0100 blanchet honor the default max relevant facts setting from the SMT solvers in Sledgehammer
Mon, 06 Dec 2010 11:25:21 +0100 blanchet have SMT solvers report the number of facts that they should have by default in Sledgehammer -- the information might not seem to belong there but it also belongs nowhere else, for how is Sledgehammer to know how different solvers deal with hundreds of facts?
Mon, 06 Dec 2010 10:32:39 +0100 blanchet return all facts for CVC3 and Yices, since there is no proof parsing / unsat core extraction
Mon, 06 Dec 2010 10:31:29 +0100 blanchet trust SMT filter's timeout -- nested timeouts seem to be at the origin of spontaneous Interrupt exceptions in some cases
Mon, 06 Dec 2010 10:23:31 +0100 blanchet reraise interrupt exceptions
Mon, 06 Dec 2010 09:54:58 +0100 blanchet [mq]: sledge_binary_minimizer
Mon, 06 Dec 2010 10:52:48 +0100 bulwahn correcting usage documentation in mirabelle tool
Mon, 06 Dec 2010 10:52:46 +0100 bulwahn adding mutabelle as a component and an isabelle tool to be used in regression testing
(0) -30000 -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip