[isabelle] strange behaviour with type instantiation

Dear all,

I'd like to do the following standard type instantiation:


instantiation  list :: (type) ord

definition le_list_def : "s \<le> t \<longleftrightarrow> (\<exists> r. s @ r = t)" definition less_list_def: "s < t \<longleftrightarrow> s \<le> t \<and> s \<noteq> t"

definition less_list_def : "less \<equiv> \<lambda> x y. (x \<le> y \<and> x \<noteq> y)"
instance  ..


However, I got the following respionse (under Isabelle 2008):

*** Bad head of lhs: existing constant "op <"
*** The error(s) above occurred in definition: "s < t  s ~ t ~ s ~ t"
*** At command "definition".

Exchanging the offending s < t by the core notation (see comments)
no avail.

Can anyone help me out ?

Best regards,


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