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?
I don't have the original sources at hand, but it was something like this:
consts my_overloaded_const :: "(int * 'a)" definition foo :: "int ⇒ int" where "foo x = x + fst my_overloaded_const" But what Isabelle gives back is foo :: 'a itself ⇒ int ⇒ intwhich is neither a generalization nor a specialization of the type signature we gave it. Originally this was part of some automatically- generated Isabelle theories, so we didn't see any of the warning messages.
Instead, Isabelle started giving us (what we thought were) strange type errors when we started using the constant in theories that inherited from the automatically generated theory.
We figured out what was going on and fixed the translator, but it would have saved us time and confusion if Isabelle had stopped and given us an error when we tried to define foo.
-john
smime.p7s
Description: S/MIME cryptographic signature
_______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
