Wed, 28 Apr 2010 16:03:49 +0200 reintroduced short names for HOL->FOL constants; other parts of the code rely on these
blanchet [Wed, 28 Apr 2010 16:03:49 +0200] rev 36493
reintroduced short names for HOL->FOL constants; other parts of the code rely on these
Wed, 28 Apr 2010 15:53:17 +0200 save the name of Skolemized variables in Sledgehammer for use in the proof reconstruction code
blanchet [Wed, 28 Apr 2010 15:53:17 +0200] rev 36492
save the name of Skolemized variables in Sledgehammer for use in the proof reconstruction code
Wed, 28 Apr 2010 15:34:55 +0200 unskolemize formulas in proof reconstruction + detect newer SPASS versions to avoid truncating identifiers if not necessary (truncating confuses proof reconstruction)
blanchet [Wed, 28 Apr 2010 15:34:55 +0200] rev 36491
unskolemize formulas in proof reconstruction + detect newer SPASS versions to avoid truncating identifiers if not necessary (truncating confuses proof reconstruction)
(0) -30000 -10000 -3000 -1000 -300 -100 -30 -10 -3 +3 +10 +30 +100 +300 +1000 +3000 +10000 +30000 tip