[isabelle] Morphism locales and interpretations [SEC=UNCLASSIFIED]



Apologies for what may be a trivial question, but a quick look through the HOL sources and this list has not offered anything useful examples.

I have a a locale topology (many details omitted) with an interpretation real_top: topology "UNIV::real set" "real_top"

I also have a locale continuous_fun = A: topology A S + B: topology B S fixes f :: "'a => 'b".

When I try to 

interpret continuous_fun A S "UNIV::real set" "real_top" f 

I get an unhelpful error message 

exception DUP ...
  
which seems to be complaining that  the real_top interpretation is being duplicated. If I instead use 

interpret continuous_fun A S "UNIV::real set" "id real_top"

there is no problem with DUP, but of course I don't have exactly the interpretation I want.

Is there any way to get around this DUP exception?

Brendan


------------------------------------------------------------------  
Dr Brendan Mahony
C3I Division                                    ph +61 8 7389 6046
Defence Science and Technology Organisation     fx +61 8 7389 5589
Edinburgh, South Australia      Brendan.Mahony at dsto.defence.gov.au

Important: This document remains the property of the Australian 
Government Department of Defence and is subject to the jurisdiction 
of the Crimes Act section 70. If you have received this document in
error, you are requested to contact the sender and delete the document.




IMPORTANT: This email remains the property of the Department of Defence and is subject to the jurisdiction of section 70 of the Crimes Act 1914. If you have received this email in error, you are requested to contact the sender and delete the email.




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.