[isabelle-dev] Additional type variable(s) in specification
makarius at sketis.net
Thu Dec 2 20:42:22 CET 2010
On Thu, 2 Dec 2010, John Matthews wrote:
> As another user data point, a few months back I ran into this same issue
> of the type I specified not being the type Isabelle gave me back. It was
> pretty confusing at the time and it took me a while to figure out what
> was going on.
Sorry, I don't quite get it.
What you specify is a type constraint for the main body of the
specification text. There can be a mismatch of what the system infers as
most general type and what you've had in mind. There can be also
surprises due to type abbreviations.
Which situation did you have exactly?
More information about the isabelle-dev