[isabelle-dev] Clash of specifications

Amine Chaieb ac638 at cam.ac.uk
Fri Jul 3 12:23:51 CEST 2009

Dear all,

I woul like to merge a few theories and already at the theory - imports
declaration I get the following error message:

*** Clash of specifications "Sign.sign.size_sign_inst.size_sign_def" and
"Sign.sign.size_sign_inst.size_sign_def" for constant "Nat.size_class.size"
*** At command "theory".

Is this similar to the typerep issue? Any explanations? Workarounds?

Best wishes,


More information about the isabelle-dev mailing list