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

Dr. Brendan Patrick Mahony wrote:
> 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.

Hi Brendan,

when porting the theories in the Isabelle distribution to the new encoding
of sets as predicates, we found that most of the instance proofs for sets
could be replaced by appropriate instance proofs for functions and booleans
in a rather straightforward way. Could you give an example of an instance proof
for sets that you could not easily replace by instance proofs for functions and


Dr. Stefan Berghofer               E-Mail: berghofe at
Institut fuer Informatik           Phone: +49 89 289 17328
Technische Universitaet Muenchen   Fax:   +49 89 289 17307
Boltzmannstr. 3                    Room: 01.11.059
85748 Garching, GERMANY  

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