We certainly need to solve this problem. One possible criterion: which results 
are part of a standard undergraduate  athematics curriculum?

> 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.

Attachment: signature.asc
Description: Message signed with OpenPGP

isabelle-dev mailing list

Reply via email to