[isabelle] typedecl vs. type synonym
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and