Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. merged
  2. merged
  3. de-applying
  4. HOL-Analysis: Volume of a simplex, Heron's theorem
  5. Tagged Ball_Volume and Gamma_Function in HOL-Analysis
  6. correct import
  7. merged
  8. unit_cube = cbox 0 One
  9. relaxed assumptions for dim_image_eq and dim_image_le
  10. merged
  11. de-applying (mostly Set_Interval)
Changeset 68628:958511f53de8 by paulson:
merged
Changeset 68627:e371784becd9 by paulson:
merged
Changeset 68626:330c0ec897a4 by paulson _lp15@cam.ac.uk_:
de-applying
The file was modified src/HOL/Divides.thy (diff)
The file was modified src/HOL/Vector_Spaces.thy (diff)
Changeset 68625:2ec84498f562 by manuel eberl _eberlm@in.tum.de_:
HOL-Analysis: Volume of a simplex, Heron's theorem
The file was addedsrc/HOL/Analysis/Simplex_Content.thy
The file was modified src/HOL/Analysis/Analysis.thy (diff)
Changeset 68624:205d352ed727 by manuel eberl _eberlm@in.tum.de_:
Tagged Ball_Volume and Gamma_Function in HOL-Analysis
The file was modified src/HOL/Analysis/Ball_Volume.thy (diff)
The file was modified src/HOL/Analysis/Gamma_Function.thy (diff)
Changeset 68623:b942da0962c2 by nipkow:
correct import
The file was modified src/HOL/Analysis/Inner_Product.thy (diff)
The file was modified src/HOL/Computational_Algebra/Primes.thy (diff)
Changeset 68622:0987ae51a3be by nipkow:
merged
Changeset 68621:27432da24236 by nipkow:
unit_cube = cbox 0 One
The file was modified src/HOL/Analysis/Brouwer_Fixpoint.thy (diff)
Changeset 68620:707437105595 by immler:
relaxed assumptions for dim_image_eq and dim_image_le
The file was modified src/HOL/Analysis/Euclidean_Space.thy (diff)
The file was modified src/HOL/Types_To_Sets/Examples/Linear_Algebra_On.thy (diff)
The file was modified src/HOL/Types_To_Sets/Examples/Linear_Algebra_On_With.thy (diff)
The file was modified src/HOL/Vector_Spaces.thy (diff)
Changeset 68619:79abf4201e8d by paulson:
merged
Changeset 68618:3db8520941a4 by paulson _lp15@cam.ac.uk_:
de-applying (mostly Set_Interval)
The file was modified src/HOL/Nat.thy (diff)
The file was modified src/HOL/Set_Interval.thy (diff)
The file was modified src/HOL/Transitive_Closure.thy (diff)