Hi Amine, I guess you are in the following thygraph situation:
Typrep Real | / \ | |/ \| Complex_Main FPS \ / \ / \ / Foo Real defines type real, Typerep class typerep (;-)). Then both in Complex_Main and FPS and instance for typerep on type real is generated automatically (thanks to generic interpretation), which clash on merge into theory Foo. The solution is too arrange that there is only one meeting point of Typrep and Real in the thygraph. According to your second email you have already found a way. N.B. arranging the HOL thygraph is a nontrivial task! Cheers, Florian Amine Chaieb schrieb: > This behaviour is even more strange than I thought. >=20 >=20 > I am trying to merge my theory with Complex_Main . The latter looks lik= e: >=20 >=20 > theory Complex_Main >=20 > imports > Main > Real > Fundamental_Theorem_Algebra > Log > Ln > Taylor > Integration > FrechetDeriv > begin >=20 > end >=20 >=20 > 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? >=20 >=20 > Best wishes, >=20 > Amine. >=20 >=20 > Amine Chaieb wrote: >=20 >> 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/isabell= e-dev >> =20 > _______________________________________________ > Isabelle-dev mailing list > Isabelle-dev at mailbroy.informatik.tu-muenchen.de > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle= -dev --=20 Home: http://wwwbroy.in.tum.de/~haftmann PGP available: http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_in= formatik_tu_muenchen_de -------------- next part -------------- A non-text attachment was scrubbed... Name: signature.asc Type: application/pgp-signature Size: 252 bytes Desc: OpenPGP digital signature URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20090120/362dc67f/attachment.pgp>