[isabelle] Type class instantiation without using Isar syntax
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.
The sample file I am working with is
imports Main "Quotient"
datatype MyType = A | B
eq :: "MyType => MyType => bool"
primrec "eq A y = (y = A)"
"eq B y = (y = B)"
instance MyType:: eqv
myType_sim_def : "eqv x y == (eq x y)"
instance MyType:: equiv
apply (unfold myType_sim_def)
This archive was generated by a fusion of
Pipermail (Mailman edition) and