ac638 at cam.ac.uk
Tue Jan 20 16:00:42 CET 2009
When I try to merge two theories I get this (to me new) error message:
*** Clash of specifications
"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.
More information about the isabelle-dev