[isabelle] typedecl vs. type synonym



Hi,

I currently have two formalizations of the same pen and paper model in
Isabelle.  In one of the formalizations type variables are used
extensively to formalize "underspecified sets" from the pen & paper
model.  In the other formalization the "underspecified sets" are
formalized with typedecl.

Now I try to get an idea what the advantages of the two approaches are,
but I cannot find a suitable starting point for this in the Isabelle
documentation.  Any hints?  A short reply when to use which style would
also be very welcome.

Thanks,
Matthias




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.