Re: [isabelle] Why no HOL set type in 2008?



The latest problem encountered in in developing instances of  
axclasses. No set type means no set instance claims for axclasses.  
Obviously function type instance proofs are very different.

Brendan

On 16/12/2008, at 5:12 PM, Tobias Nipkow wrote:

> Brendan, you are certainly right that in some situations proofs are  
> less
> automatic. We were aware of this but found that in the theories we  
> have
> access to it was not too bad, only a few times per theory on average.
> However we concede that depending on your application this could be
> worse. I'm very sorry if you were particularly affected.



------------------------------------------------------------------
Dr Brendan Mahony
C3I Division                                    ph +61 8 8259 6046
Defence Science and Technology Organisation     fx +61 8 8259 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 Australian Defence Organisation 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.