[isabelle] Axclass with multiple type variables?



Dear all,

would there be any way of using multiple type variables in an axclass, e.g. in a cascaded definition like this:

axclass A \<subseteq> type

consts
f :: "'a::A \<Rightarrow> 'b \<Rightarrow> bool"
axclass B \<subseteq> type
f_holds: "f a b"

Here, the error message of course is

*** Multiple type variables in class axiom:
*** f a b
*** At command "axclass".

Is there any solution to establish the above construction in Isabelle?

Thanks in advance,

Nicole






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