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.
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 in.tum.de
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 http://www.in.tum.de/~berghofe
This archive was generated by a fusion of
Pipermail (Mailman edition) and