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
Mon, 06 Dec 2010 10:52:45 +0100 bulwahn commenting out sledgehammer_mtd in Mutabelle
Mon, 06 Dec 2010 10:52:45 +0100 bulwahn removing declaration in quickcheck to really enable exhaustive testing
Mon, 06 Dec 2010 10:52:44 +0100 bulwahn adding timeout to try invocation in mutabelle
Mon, 06 Dec 2010 10:52:43 +0100 bulwahn adding filtering, sytactic welltyping, and sledgehammer method in mutabelle
Mon, 06 Dec 2010 09:34:57 +0100 haftmann replace `type_mapper` by the more adequate `type_lifting`
Mon, 06 Dec 2010 09:25:05 +0100 haftmann moved bootstrap of type_lifting to Fun
Mon, 06 Dec 2010 09:19:10 +0100 haftmann replace `type_mapper` by the more adequate `type_lifting`
Mon, 06 Dec 2010 14:45:29 +0100 wenzelm avoid explicit encoding -- acknowledge UTF-8 as global default and Isabelle/jEdit preference of UTF-8-Isabelle;
Sun, 05 Dec 2010 15:23:33 +0100 wenzelm IsabelleText font: include Cyrillic, Hebrew, Arabic from DejaVu Sans 2.32;
Sun, 05 Dec 2010 14:02:16 +0100 wenzelm command 'notepad' replaces former 'example_proof';
(0) -30000 -10000 -3000 -1000 -300 -100 -16 +16 +100 +300 +1000 +3000 +10000 +30000 tip