[isabelle] strange behaviour with type instantiation



Dear all,

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

>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>

instantiation  list :: (type) ord
begin

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  ..

end

<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<
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,

bu





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