Thu, 10 May 2012 10:07:40 +0200 use raw monomorphic encoding with Waldmeister, to avoid overloading it with too many function symbols (as would be the case using mangled monomorphic encodings)
blanchet [Thu, 10 May 2012 10:07:40 +0200] rev 47898
use raw monomorphic encoding with Waldmeister, to avoid overloading it with too many function symbols (as would be the case using mangled monomorphic encodings)
Wed, 09 May 2012 11:24:38 +0200 build Pure_64 with new settings
bulwahn [Wed, 09 May 2012 11:24:38 +0200] rev 47897
build Pure_64 with new settings
Wed, 09 May 2012 11:17:54 +0200 tuned
bulwahn [Wed, 09 May 2012 11:17:54 +0200] rev 47896
tuned
Wed, 09 May 2012 10:39:54 +0200 playing around with mira settings
bulwahn [Wed, 09 May 2012 10:39:54 +0200] rev 47895
playing around with mira settings
Tue, 08 May 2012 14:35:13 +0200 defining and proving Executable_Relation with lift_definition and transfer
bulwahn [Tue, 08 May 2012 14:35:13 +0200] rev 47894
defining and proving Executable_Relation with lift_definition and transfer
Tue, 08 May 2012 14:31:03 +0200 specialised fact in the Record theory should not be appear in proofs discovered by sledgehammer
bulwahn [Tue, 08 May 2012 14:31:03 +0200] rev 47893
specialised fact in the Record theory should not be appear in proofs discovered by sledgehammer
Mon, 07 May 2012 14:50:49 +0200 prevent spurious timeouts
blanchet [Mon, 07 May 2012 14:50:49 +0200] rev 47892
prevent spurious timeouts
Mon, 07 May 2012 12:20:55 +0200 added "try0" tool to Mirabelle
blanchet [Mon, 07 May 2012 12:20:55 +0200] rev 47891
added "try0" tool to Mirabelle
Mon, 07 May 2012 12:20:55 +0200 use latest E (1.5)
blanchet [Mon, 07 May 2012 12:20:55 +0200] rev 47890
use latest E (1.5)
Fri, 04 May 2012 17:12:37 +0200 lifting package produces abs_eq_iff rules for total quotients
huffman [Fri, 04 May 2012 17:12:37 +0200] rev 47889
lifting package produces abs_eq_iff rules for total quotients
(0) -30000 -10000 -3000 -1000 -300 -100 -10 +10 +100 +300 +1000 +3000 +10000 tip