Re: [isabelle] Questions about theories distributed with Isabelle



Hi Josh,

> First, the
README<http://isabelle.in.tum.de/dist/library/HOL/HOL-Algebra/README.html>
> refers
> to type-classes disparagingly. Does the Isabelle community at large believe
> that "axiomatic type classes" cannot be "first-class citizens of the
> logic"? If so, I'd be interested to know *why* that's the case, but it's
> not required so don't spend too much time explaining.
> 
> Second, many of the theories listed in HOL-Algebra are topically similar to
> theories included in HOL's Main. Why are they split out?

as a rule of thumb, there are basically two algebraic hierarchy
developments in HOL:

HOL-Main with type classes:
* implicit use due to type inference
* pragmatic and simple sharing between similar types
* explicit definitions
* directly executable
* …

HOL-Algebra with locales:
* explicit carrier – possibility to develop proper meta theory
* implicit definitions where possible
* suitable for mathematics

Hope this helps,
	Florian

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

Attachment: signature.asc
Description: OpenPGP digital signature



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