ac638 at cam.ac.uk
Tue Jan 20 16:56:11 CET 2009
This behaviour is even more strange than I thought.
I am trying to merge my theory with Complex_Main . The latter looks like:
Now when I merge my theory with all the theories imorted by
Complex_Main, it works. Is this behaviour really intended? Maybe I
Amine Chaieb wrote:
> Dear all,
> When I try to merge two theories I get this (to me new) error message:
> *** Clash of specifications
> "Complex_Main.typerep_real_inst.typerep_real_def" and
> "FPS.typerep_real_inst.typerep_real_def" for constant
> *** At command "theory".
> What does it mean? I do not mention typerep, nor typerep_real, no real
> at all. I guess it has something to do with the typedef package, but
> what is it?
> Any hint is welcome.
> Best wishes,
> Isabelle-dev mailing list
> Isabelle-dev at mailbroy.informatik.tu-muenchen.de
More information about the isabelle-dev