[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 
*** 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 

I would be happy with the ugliest hack.


More information about the isabelle-dev mailing list