Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. Loads of new material related to porting the Euler Polyhedron Formula from HOL Light
  2. merged
  3. merged
  4. tidying up old apply-style proofs
Changeset 78656:4da1e18a9633 by paulson _lp15@cam.ac.uk_:
Loads of new material related to porting the Euler Polyhedron Formula from HOL Light
The file was modified src/HOL/Analysis/Convex.thy (diff)
The file was modified src/HOL/Analysis/Lebesgue_Measure.thy (diff)
The file was modified src/HOL/Analysis/Linear_Algebra.thy (diff)
The file was modified src/HOL/Analysis/Polytope.thy (diff)
The file was modified src/HOL/Analysis/Starlike.thy (diff)
The file was modified src/HOL/Binomial.thy (diff)
The file was modified src/HOL/Real_Vector_Spaces.thy (diff)
Changeset 78655:0d065af1a99c by paulson:
merged
Changeset 78654:af34c689bfda by paulson:
merged
Changeset 78653:7ed1759fe1bd by paulson _lp15@cam.ac.uk_:
tidying up old apply-style proofs
The file was modified src/HOL/Data_Structures/Array_Braun.thy (diff)
The file was modified src/HOL/Data_Structures/Brother12_Set.thy (diff)
The file was modified src/HOL/Data_Structures/Sorting.thy (diff)
The file was modified src/HOL/Data_Structures/Tries_Binary.thy (diff)