Re: [isabelle] New in the AFP: Intersecting Chords Theorem



I havenât come across any. The most distinctive feature of HOL Light is its suite of âwithout loss of generalityâ tactics, which however seldom seem to lead to shorter or more readable proofs.

Larry

> On 14 Oct 2016, at 08:17, Tobias Nipkow <nipkow at in.tum.de> wrote:
> 
> All of the ones that Johannes says can be proved by GrÃbner bases have been proved in HOL Light, which has well-developed GrÃbner basis algorithms. It would be interesting to see if the proofs make use of them.
> 
> Tobias





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