Wed, 30 Jul 2014 14:03:12 +0200 imported patch satallax_proof_support_Sledgehammer
fleury [Wed, 30 Jul 2014 14:03:12 +0200] rev 57707
imported patch satallax_proof_support_Sledgehammer
Wed, 30 Jul 2014 14:03:12 +0200 Basic support for the higher-order ATP Satallax.
fleury [Wed, 30 Jul 2014 14:03:12 +0200] rev 57706
Basic support for the higher-order ATP Satallax.
Wed, 30 Jul 2014 14:03:12 +0200 Subproofs for the SMT solver veriT.
fleury [Wed, 30 Jul 2014 14:03:12 +0200] rev 57705
Subproofs for the SMT solver veriT.
Wed, 30 Jul 2014 14:03:12 +0200 Basic support for the SMT prover veriT.
fleury [Wed, 30 Jul 2014 14:03:12 +0200] rev 57704
Basic support for the SMT prover veriT.
Wed, 30 Jul 2014 14:03:11 +0200 removing the '= True' generated by Leo-II.
fleury [Wed, 30 Jul 2014 14:03:11 +0200] rev 57703
removing the '= True' generated by Leo-II.
Wed, 30 Jul 2014 14:03:11 +0200 Skolemization support for leo-II and Zipperposition.
fleury [Wed, 30 Jul 2014 14:03:11 +0200] rev 57702
Skolemization support for leo-II and Zipperposition.
Wed, 30 Jul 2014 10:50:30 +0200 document property 'set_induct'
desharna [Wed, 30 Jul 2014 10:50:30 +0200] rev 57701
document property 'set_induct'
Wed, 30 Jul 2014 10:50:28 +0200 generate 'set_induct' theorem for codatatypes
desharna [Wed, 30 Jul 2014 10:50:28 +0200] rev 57700
generate 'set_induct' theorem for codatatypes
Wed, 30 Jul 2014 00:50:41 +0200 also try 'metis' with 'full_types'
blanchet [Wed, 30 Jul 2014 00:50:41 +0200] rev 57699
also try 'metis' with 'full_types'
Tue, 29 Jul 2014 23:39:35 +0200 header tuning
blanchet [Tue, 29 Jul 2014 23:39:35 +0200] rev 57698
header tuning
(0) -30000 -10000 -3000 -1000 -300 -100 -10 +10 +100 +300 +1000 +3000 +10000 tip