Re: [isabelle] Generating fresh type variables
On Wed, 29 Jun 2011, Mathieu Giorgino wrote:
Thanks Sascha and Christian,
I used "Variable.variant_fixes" and it worked great.
I had already used "Variable.variant_frees" for terms, but I hadn't
realized it can also be used for types. If I understand correctly, type
variables and term variables are in the same namespace (implicitly
separated by the prefix "'") ?
No you should not do that. Term variables and type variables are
different things. You probably mean Variable.invent_types, or even the
import operations that will put things into context without manual
By the way, thanks for the Isabelle Cookbook, it's really helpful to
start with Isabelle/ML.
It is certainly helpful, but you always need to cross-check with other
sources of information. Many fine points in the cookbook are not exactly
This archive was generated by a fusion of
Pipermail (Mailman edition) and