On Wed, 2 Apr 2008, Amine Chaieb wrote: > Library/Numeral_Type by Brian is what I need.
Indeed it is. > I was wondering why it depends on InfiniteSet (ATP_Linkup is perfectly > sufficient, I will commit it shortly). It at least used to depend on some lemmas about "finite" in InfiniteSet. Quite possible that it does not any more. > PS: Can't we have metis at earlier stage than ATP_Linkup?. I have > experienced many lemmas not proved by blast and auto but within seconds > by metis. I really should try these first order tactics more often.. Gerwin
