Fri, 14 May 2010 23:34:24 +0200 blanchet added Sledgehammer documentation to TOC
Fri, 14 May 2010 23:32:48 +0200 blanchet added some Sledgehammer news
Fri, 14 May 2010 23:16:33 +0200 blanchet document Nitpick changes
Fri, 14 May 2010 22:43:24 +0200 blanchet merge
Fri, 14 May 2010 22:43:00 +0200 blanchet added Sledgehammer manual;
Fri, 14 May 2010 22:30:24 +0200 blanchet renamed Sledgehammer options
Fri, 14 May 2010 22:29:50 +0200 blanchet renamed options
Fri, 14 May 2010 22:28:39 +0200 blanchet remove support for crashing beta solver HaifaSat
Fri, 14 May 2010 16:15:10 +0200 blanchet renamed two Sledgehammer options
Fri, 14 May 2010 22:46:58 +0200 nipkow merged
Fri, 14 May 2010 22:46:41 +0200 nipkow added listsum lemmas
Fri, 14 May 2010 21:23:29 +0200 ballarin Revert mixin patch due to inacceptable performance drop.
Fri, 14 May 2010 15:27:07 +0200 blanchet add "no_atp"s to Nitpick lemmas
Fri, 14 May 2010 15:26:26 +0200 blanchet query _HOME environment variables at run-time, not at build-time
Fri, 14 May 2010 15:09:37 +0200 blanchet move Refute dependency from Plain to Main
Fri, 14 May 2010 15:07:53 +0200 blanchet move Nitpick files from "PLAIN_DEPENDENCIES" to "MAIN_DEPENDENCIES", where they belong
Fri, 14 May 2010 15:02:38 +0200 blanchet recognize new Kodkod error message syntax
Fri, 14 May 2010 14:14:22 +0200 blanchet improve precision of set constructs in Nitpick
Fri, 14 May 2010 12:01:16 +0200 blanchet produce more potential counterexamples for subset operator (cf. quantifiers)
Fri, 14 May 2010 11:24:49 +0200 blanchet improved Sledgehammer proofs
Fri, 14 May 2010 11:24:14 +0200 blanchet pass "full_type" argument to proof reconstruction
Fri, 14 May 2010 11:23:42 +0200 blanchet made Sledgehammer's full-typed proof reconstruction work for the first time;
Fri, 14 May 2010 11:20:09 +0200 blanchet delect installed ATPs dynamically, _not_ at image built time
Thu, 13 May 2010 15:09:42 +0200 ballarin Fix syntax; apparently constant apply was introduced in an earlier changeset.
Thu, 13 May 2010 14:47:15 +0200 ballarin Merged.
Thu, 13 May 2010 13:30:16 +0200 ballarin Add mixin to base morphism, required by class package; cf ab324ffd6f3d.
Thu, 13 May 2010 13:29:43 +0200 ballarin Remove improper use of mixin in class package.
Thu, 13 May 2010 14:34:05 +0200 nipkow Multiset: renamed, added and tuned lemmas;
Wed, 12 May 2010 22:33:10 -0700 huffman use 'subsection' instead of 'section', to maintain 1 chapter per file in generated document
Thu, 13 May 2010 00:44:48 +0200 boehmes more precise dependencies
(0) -30000 -10000 -3000 -1000 -300 -100 -50 -30 +30 +50 +100 +300 +1000 +3000 +10000 +30000 tip