This behaviour is even more strange than I thought.
I am trying to merge my theory with Complex_Main . The latter looks like: theory Complex_Main imports Main Real Fundamental_Theorem_Algebra Log Ln Taylor Integration FrechetDeriv begin end Now when I merge my theory with all the theories imorted by Complex_Main, it works. Is this behaviour really intended? Maybe I should reboot? Best wishes, Amine. 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 > "Typerep.typerep_class.typerep" > > *** 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, > > Amine. > > _______________________________________________ > Isabelle-dev mailing list > Isabelle-dev at mailbroy.informatik.tu-muenchen.de > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev >
