[isabelle] typedecl versus explicit type parameters
The Isabelle tutorial mentions typedecl as a simple way to say that a
type is actually a parameter to some theory development. In particular,
explicit type parameters for constants, datatypes etc. do not clutter
the definitions and proofs.
But what if later on, I want to instantiate such a type to a concrete
type in some application that uses the theory? Can this be done? If so,
can different theories instantiate the type differently? What happens
then at a theory merge?
Are there other ways to fix type parameters such that I don't have to
write them everywhere?
This archive was generated by a fusion of
Pipermail (Mailman edition) and