[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