[isabelle-dev] typrep?

[Amine Chaieb]

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
>