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 supersedes most of the HOL Light proofs (many files), which are devoted to developing the arithmetic and topological properties of quaternions. In the course of this, I also ported the HOL Light development of the three-dimensional vector cross product. So where does this material belong? Arguably not in Analysis, which is already too large. Another question: I did not port the quaternion material relating to the constant reflect_along, which is defined as follows: (* Reflection of a vector about 0 along a line. *) 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 _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
smime.p7s
Description: S/MIME Cryptographic Signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
