[isabelle-dev] Numbers in Types

Gerwin Klein gerwin.klein at nicta.com.au
Wed Apr 2 23:07:36 CEST 2008

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..


More information about the isabelle-dev mailing list