We certainly need to solve this problem. One possible criterion: which results are part of a standard undergraduate athematics curriculum? Larry
> On 18 Jan 2018, at 10:06, Fabian Immler <imm...@in.tum.de> wrote: > > We do not have a precise specification of what HOL-Analysis is or should be. > I think that makes it very hard to draw a line between material that should > go to HOL-Analysis and what should remain in the AFP. So take this as just my > personal view.
signature.asc
Description: Message signed with OpenPGP
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
