[isabelle] Type class instantiation without using Isar syntax



Hi,

I have recently migrated to Isabelle 2009. I have a Haskell code base that
produces Isabelle code automatically, however it does not produce Isar code.
Since the migration to Isabelle 2009, my instantiation of the Quotient class
does not work, where it used to work in 2008.

Could someone please help me with the code below and show me the new correct
syntax in plain Isabelle. Once this goes through then I will be able to
apply the same syntax to my Haskell code base (currently migrating the
codebase to Isar is far too much work and I don't have the time).

The error I get is on the defs line. The error is:
*** Clash of specifications "test.myType_sim_def" and
"test.eqv_MyType_inst.eqv_MyType_def" for constant "Quotient.eqv_class.eqv"
*** The error(s) above occurred in definition "myType_sim_def":
***   "x ~ y == eq x y"
*** At command "defs".

Any help will be most appreciated.

Thanks
Liam

The sample file I am working with is
--------------------
theory test
imports Main "Quotient"
begin

datatype MyType = A | B

consts
eq :: "MyType => MyType => bool"

primrec "eq A y = (y = A)"
        "eq B y = (y = B)"

instance MyType:: eqv
  by (intro_classes)

defs (overloaded)
  myType_sim_def : "eqv x y == (eq x y)"

instance MyType:: equiv
  apply (intro_classes)
  apply (unfold myType_sim_def)
  apply (auto)
  done

end




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