[isabelle-dev] typrep?

Amine Chaieb ac638 at cam.ac.uk
Tue Jan 20 16:00:42 CET 2009


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.



More information about the isabelle-dev mailing list