*To*: Tobias Nipkow <nipkow at in.tum.de>*Subject*: Re: [isabelle] New in the AFP: Intersecting Chords Theorem*From*: Lawrence Paulson <lp15 at cam.ac.uk>*Date*: Fri, 14 Oct 2016 11:41:13 +0100*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <9a301762-8775-9c26-3989-63626c00aa70@in.tum.de>*References*: <a698e11d-80b4-82c8-04cf-149399376cc5@htwk-leipzig.de> <92be815c-1412-d7a3-775f-37ef9323b9c1@in.tum.de> <9a301762-8775-9c26-3989-63626c00aa70@in.tum.de>

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

**References**:**Re: [isabelle] New in the AFP: Intersecting Chords Theorem***From:*Johannes Waldmann

**Re: [isabelle] New in the AFP: Intersecting Chords Theorem***From:*Manuel Eberl

**Re: [isabelle] New in the AFP: Intersecting Chords Theorem***From:*Tobias Nipkow

- Previous by Date: Re: [isabelle] New in the AFP: Intersecting Chords Theorem
- Next by Date: [isabelle] Foundations of Mathematics: Type Theory after Church's Simple Theory of Types (1940)
- Previous by Thread: Re: [isabelle] New in the AFP: Intersecting Chords Theorem
- Next by Thread: Re: [isabelle] New in the AFP: Intersecting Chords Theorem
- Cl-isabelle-users October 2016 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list