[isabelle-dev] Typerep again
Amine Chaieb
ac638 at cam.ac.uk
Mon Feb 9 14:59:13 CET 2009
Dear all,
I have a theory development which used to work not a long time ago. I am
now trying to include it into the distribution.
At some point I can not merge the theories and get:
*** Clash of specifications "Permutations.typerep_^_inst.typerep_^_def"
and "Misc.typerep_^_inst.typerep_^_def" for constant
"Typerep.typerep_class.typerep"
*** At command "theory".
Since an etiologic solution does not seem to exist, can you give a way
to come around these situations temporarily. They just cost time and
nerves...
I would be happy with the ugliest hack.
Amine.
More information about the isabelle-dev
mailing list