Fri, 15 Feb 2013 09:41:25 +0100 Andreas Lochbihler partially revert 0dac0158b8d4 as it too aggressively spreads card_UNIV type class whose dictionary constructions can slow down generated code;
Fri, 15 Feb 2013 09:17:26 +0100 blanchet killed legacy alias
Fri, 15 Feb 2013 09:17:20 +0100 blanchet updated news
Fri, 15 Feb 2013 09:17:20 +0100 blanchet avoid crude/wrong theorem comparision
Fri, 15 Feb 2013 09:17:20 +0100 blanchet tuned code
Fri, 15 Feb 2013 09:17:20 +0100 blanchet more MaSh tracing
Fri, 15 Feb 2013 09:17:20 +0100 blanchet tuning
Thu, 14 Feb 2013 23:54:46 +0100 smolkas fixed metis_steps_total - was off by one
Thu, 14 Feb 2013 22:49:22 +0100 smolkas preplay subblocks
Thu, 14 Feb 2013 22:49:22 +0100 smolkas renamed sledgehammer_shrink to sledgehammer_compress
Thu, 14 Feb 2013 22:49:22 +0100 smolkas dont skolemize conjecture
Thu, 14 Feb 2013 22:49:22 +0100 smolkas introduced subblock in isar_step datatype for conjecture herbrandization
Thu, 14 Feb 2013 21:31:25 +0100 wenzelm write_pdf for JFreeChart;
Thu, 14 Feb 2013 15:27:10 +0100 haftmann reform of predicate compiler / quickcheck theories:
Thu, 14 Feb 2013 17:58:28 +0100 Andreas Lochbihler merged
(0) -30000 -10000 -3000 -1000 -300 -100 -15 +15 +100 +300 +1000 +3000 +10000 +30000 tip