[isabelle-dev] Numbers in Types

[Gerwin Klein]

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