Skip to content
Success

Changes

Summary

  1. another big cleanup
  2. merged
  3. minor typeclass generalisations and junk removal
  4. merged
  5. more messy proofs
Changeset 68052:e98988801fa9 by paulson _lp15@cam.ac.uk_:
another big cleanup
The file was modified src/HOL/Analysis/Convex_Euclidean_Space.thy (diff)
Changeset 68051:68def9274939 by paulson:
merged
Changeset 68050:7eacc812ad1c by paulson _lp15@cam.ac.uk_:
minor typeclass generalisations and junk removal
The file was modified src/HOL/Analysis/Cartesian_Euclidean_Space.thy (diff)
The file was modified src/HOL/Analysis/Determinants.thy (diff)
Changeset 68049:1df89db6f162 by paulson:
merged
Changeset 68048:0b4fb9fd91b1 by paulson _lp15@cam.ac.uk_:
more messy proofs
The file was modified src/HOL/Analysis/Convex_Euclidean_Space.thy (diff)