[isabelle-dev] quaternions

Lawrence Paulson lp15 at cam.ac.uk
Mon Jun 18 14:31:28 CEST 2018


The cross product development is 200 lines long while the quaternion development is 730. Should they be separate entries, or do cross products belong elsewhere?
Larry

> On 18 Jun 2018, at 13:18, Tobias Nipkow <nipkow at in.tum.de> wrote:
> 
> Why not simply the AFP?

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 833 bytes
Desc: Message signed with OpenPGP
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20180618/ab7445e6/attachment.sig>


More information about the isabelle-dev mailing list