blanchet [Tue, 21 Jun 2011 17:17:39 +0200] rev 43501
don't change the way helpers are generated for the exporter's sake
blanchet [Tue, 21 Jun 2011 17:17:39 +0200] rev 43500
provide appropriate type system and number of fact defaults for remote ATPs
blanchet [Tue, 21 Jun 2011 17:17:39 +0200] rev 43499
order generated facts topologically
blanchet [Tue, 21 Jun 2011 17:17:39 +0200] rev 43498
peel off two or more layers in exceptional cases where the proof term refers to the proved theorems twice with the same name (e.g., "Transitive_Closure.trancl_into_trancl")
blanchet [Tue, 21 Jun 2011 17:17:39 +0200] rev 43497
tweaked E, SPASS, Vampire setup based on latest Judgment Day results
blanchet [Tue, 21 Jun 2011 17:17:39 +0200] rev 43496
remove historical bloat -- another benefit of merging Metis's and Sledgehammer's translations