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?
Makarius
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
