Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. In interpretation commands, clarify what to do with definitions immediately subject to rewriting.
  2. merged
  3. fixing overloading problems involving vector cross products
  4. corrections to markup
  5. New material in support of quaternions
Changeset 68469:aad109fde9ec by ballarin:
In interpretation commands, clarify what to do with definitions immediately subject to rewriting.
The file was modified NEWS (diff)
Changeset 68468:ae42b0f6885d by paulson:
merged
Changeset 68467:44ffc5b9cd76 by paulson _lp15@cam.ac.uk_:
fixing overloading problems involving vector cross products
The file was modified src/HOL/Analysis/Cross3.thy (diff)
The file was modified src/HOL/Product_Type.thy (diff)
Changeset 68466:3d8241f4198b by paulson _lp15@cam.ac.uk_:
corrections to markup
The file was modified CONTRIBUTORS (diff)
The file was modified NEWS (diff)
The file was modified src/HOL/Algebra/Zassenhaus.thy (diff)
The file was modified src/HOL/Analysis/Cross3.thy (diff)
Changeset 68465:e699ca8e22b7 by paulson _lp15@cam.ac.uk_:
New material in support of quaternions
The file was addedsrc/HOL/Analysis/Cross3.thy
The file was modified src/HOL/Analysis/Analysis.thy (diff)
The file was modified src/HOL/Analysis/L2_Norm.thy (diff)
The file was modified src/HOL/Analysis/Starlike.thy (diff)
The file was modified src/HOL/NthRoot.thy (diff)
The file was modified src/HOL/Real_Vector_Spaces.thy (diff)