Mon, 09 Aug 2010 14:47:28 +0200 haftmann separated foundation of `notes`
Mon, 09 Aug 2010 14:20:21 +0200 haftmann more clear separation into local and global facts
Mon, 09 Aug 2010 14:07:23 +0200 haftmann sharpened and tuned educated guess for canonical class morphism
Mon, 09 Aug 2010 13:43:01 +0200 haftmann minimize sorts in certificate instantiation
Mon, 09 Aug 2010 14:08:30 +0200 blanchet prevent ATP thread for staying around for 1 minute if an exception occurred earlier;
Mon, 09 Aug 2010 14:00:32 +0200 blanchet adapt "too_general_equality" blacklisting to the new FOF context, where quantifiers are sometimes present
(0) -30000 -10000 -3000 -1000 -300 -100 -30 -10 -6 +6 +10 +30 +100 +300 +1000 +3000 +10000 +30000 tip