[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 MHonArc.