Tue, 24 May 2011 10:03:15 +0200 pass fewer relevant facts to less used remote systems
blanchet [Tue, 24 May 2011 10:03:15 +0200] rev 42969
pass fewer relevant facts to less used remote systems
Tue, 24 May 2011 10:01:03 +0200 more work on parsing LEO-II proofs and extracting uses of extensionality
blanchet [Tue, 24 May 2011 10:01:03 +0200] rev 42968
more work on parsing LEO-II proofs and extracting uses of extensionality
Tue, 24 May 2011 10:01:00 +0200 tuning
blanchet [Tue, 24 May 2011 10:01:00 +0200] rev 42967
tuning
Tue, 24 May 2011 10:00:38 +0200 more work on parsing LEO-II proofs without lambdas
blanchet [Tue, 24 May 2011 10:00:38 +0200] rev 42966
more work on parsing LEO-II proofs without lambdas
Tue, 24 May 2011 00:01:33 +0200 slightly gracefuller handling of LEO-II and Satallax output
blanchet [Tue, 24 May 2011 00:01:33 +0200] rev 42965
slightly gracefuller handling of LEO-II and Satallax output
Tue, 24 May 2011 00:01:33 +0200 document primitive support for LEO-II and Satallax
blanchet [Tue, 24 May 2011 00:01:33 +0200] rev 42964
document primitive support for LEO-II and Satallax
Tue, 24 May 2011 00:01:33 +0200 identify HOL functions with THF functions
blanchet [Tue, 24 May 2011 00:01:33 +0200] rev 42963
identify HOL functions with THF functions
Tue, 24 May 2011 00:01:33 +0200 started adding support for THF output (but no lambdas)
blanchet [Tue, 24 May 2011 00:01:33 +0200] rev 42962
started adding support for THF output (but no lambdas)
Tue, 24 May 2011 00:01:33 +0200 eliminated more code duplication in Nitrox
blanchet [Tue, 24 May 2011 00:01:33 +0200] rev 42961
eliminated more code duplication in Nitrox
Tue, 24 May 2011 00:01:33 +0200 reduce code duplication in Nitrox
blanchet [Tue, 24 May 2011 00:01:33 +0200] rev 42960
reduce code duplication in Nitrox
(0) -30000 -10000 -3000 -1000 -300 -100 -10 +10 +100 +300 +1000 +3000 +10000 +30000 tip