# [isabelle] instantiation order for a record

Dear Isabelle community,
I am having trouble instantiation the typeclass order for one of my records.
Actually, the problem exists whenever the typeclass has parameters, to
be defined.
The error message is not particularly helpful to me.
*** Bad head of lhs: existing constant "op \<le>"
*** The error(s) above occurred in definition:
*** "A \<le> B \<equiv> lesseqTESTRECORD A B"
The online manual did not help me much in this case either; I tried
unsuccessfully to translate the examples from the manual to my case.
Hopefully somebody can give me a hint on what to change to get to the
point where the proving can start.
Cheers,
Sven
==============================
TESTRECORD.thy BEGIN
==============================
theory TESTRECORD
imports
Main
begin
record 'a TESTRECORD =
prefix_elem :: "'a set"
definition lesseqTESTRECORD :: "'a TESTRECORD \<Rightarrow> 'a
TESTRECORD \<Rightarrow> bool" where
"lesseqTESTRECORD D1 D2 \<equiv> (prefix_elem D1 \<subseteq>
prefix_elem D2)"
definition lessTESTRECORD :: "'a TESTRECORD \<Rightarrow> 'a TESTRECORD
\<Rightarrow> bool" where
"lessTESTRECORD D1 D2 \<equiv> lesseqTESTRECORD D1 D2 \<and> D1\<noteq>D2"
instantiation "TESTRECORD_ext" :: (type,type) order
begin
print_context
definition
less_eq_TESTRECORD_ext_def: "less_eq A B = lesseqTESTRECORD A B"
definition
less_TESTRECORD_ext_def: "less A B = lessTESTRECORD A B"
instance proof
==============================
TESTRECORD.thy END
==============================

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