[isabelle] How to access a locale type parameter in a quotient type definition


Consider the following attempt of a locale definition:

    locale example =
      fixes R :: "['a, 'a] ⇒ bool"
      assumes is_equivalence: "equivp R"
    quotient_type Q = 'a / R

Isabelle doesn’t accept the use of the type variable `'a` in the
quotient type definition, although it does accept referring to `'a` in
types. How can I define a quotient type for the type `'a`?

All the best,

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