Re: [isabelle] strange behaviour with type instantiation

Hi Burkhart,
> instantiation  list :: (type) ord
> begin
> definition  le_list_def  : "s \<le> t \<longleftrightarrow> (\<exists>
> r. s @ r = t)"
> definition  less_list_def: "(s::'\<alpha> list) < t
> \<longleftrightarrow> s \<le> t \<and> s \<noteq> t"

This is a misunderstanding how type variables work wrt. instantiation:
type variables for instance specifications are locally fixes during the
whole instantiation block.  Thus you have to write "'a" instead of

Hope this helps,


Attachment: signature.asc
Description: OpenPGP digital signature

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