[isabelle-dev] Numbers in Types
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