wenzelm [Tue, 21 Jun 2011 23:08:16 +0200] rev 43504
avoid fractional font metrics, which makes rendering really ugly (e.g. on Linux);
wenzelm [Tue, 21 Jun 2011 22:40:30 +0200] rev 43503
some arrow symbols from DejaVuSansMono for bsub/esub/bsup/esup;
wenzelm [Tue, 21 Jun 2011 21:34:36 +0200] rev 43502
more precise font transformations: shift sub/superscript, adjust size for user fonts;
tuned;
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
blanchet [Tue, 21 Jun 2011 17:17:39 +0200] rev 43495
avoid double ASCII-fication