[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

*** 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,


More information about the isabelle-dev mailing list