I have just formalised most of the HOL Light development of quaternions. It's a
great advertisement for type classes: showing that quaternions constitute a
real normed division algebra and an inner product space supersedes most of the
HOL Light proofs (many files), which are devoted to developin
> So where does this material belong? Arguably not in Analysis, which is
> already too large.
Why not a regular AFP entry?
Cheers
Lars
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/i
Why not simply the AFP?
Tobias
On 18/06/2018 12:36, Lawrence Paulson wrote:
I have just formalised most of the HOL Light development of quaternions. It's a
great advertisement for type classes: showing that quaternions constitute a
real normed division algebra and an inner product space super
I would also have suggested an AFP entry.
> let reflect_along = new_definition
> `reflect_along v (x:real^N) = x - (&2 * (x dot v) / (v dot v)) % v`;;
Think of it as x being the direction of a ray of light hitting a mirror
(in the shape of a hyperplane through the origin with normal vector a)
and
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 wrote:
>
> Why not simply the AFP?
signature.asc
Description: Message signed with
ine. *)
>>
>> let reflect_along = new_definition
>> `reflect_along v (x:real^N) = x - (&2 * (x dot v) / (v dot v)) % v`;;
>>
>> Is this concept useful, and if so, where does it belong?
>>
>> Larry
>>
>> __
Dear list,
the good news is that we have just received new hardware (Dual Epyc
7601).
The bad news is that a current development snapshot
(Isabelle/410818a69ee3) exhibits a problem on this hardware. In
particular, the session HOL-Corec_Examples doesn't appear to terminate.
$ cat .isabelle/
On 18/06/18 21:30, Lars Hupel wrote:
>
> the good news is that we have just received new hardware (Dual Epyc 7601).
>
> The bad news is that a current development snapshot
> (Isabelle/410818a69ee3) exhibits a problem on this hardware. In
> particular, the session HOL-Corec_Examples doesn't appear