Sun, 26 May 2013 14:02:03 +0200 blanchet disable SPASS's splitting if Isar proofs are desired, because these are not handled by the proof reconstruction code (and it's not clear how to handle them considering the lack of documentation)
Sun, 26 May 2013 12:56:37 +0200 blanchet handle lambda-lifted problems in Isar construction code
Sun, 26 May 2013 11:56:55 +0200 nipkow simpler proof through custom summation function
Sat, 25 May 2013 18:30:38 +0200 wenzelm merged
Sat, 25 May 2013 17:40:44 +0200 wenzelm tuned;
Sat, 25 May 2013 17:13:34 +0200 wenzelm tuned;
(0) -30000 -10000 -3000 -1000 -300 -100 -30 -10 -6 +6 +10 +30 +100 +300 +1000 +3000 +10000 tip