Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. more economic tagging
  2. de-applying (mostly Quotient)
  3. de-applying
Changeset 68617:75129a73aca3 by nipkow:
more economic tagging
The file was modified src/HOL/Analysis/Brouwer_Fixpoint.thy (diff)
The file was modified src/HOL/Analysis/Euclidean_Space.thy (diff)
The file was modified src/HOL/Analysis/Inner_Product.thy (diff)
The file was modified src/HOL/Analysis/Measure_Space.thy (diff)
The file was modified src/HOL/Analysis/Product_Vector.thy (diff)
The file was modified src/HOL/Analysis/Topology_Euclidean_Space.thy (diff)
The file was modified src/HOL/ROOT (diff)
Changeset 68616:cedf3480fdad by paulson _lp15@cam.ac.uk_:
de-applying (mostly Quotient)
The file was modified src/HOL/Analysis/Infinite_Products.thy (diff)
The file was modified src/HOL/Quotient.thy (diff)
Changeset 68615:3ed4ff0b7ac4 by paulson _lp15@cam.ac.uk_:
de-applying
The file was modified src/HOL/Limits.thy (diff)
The file was modified src/HOL/Quotient.thy (diff)
The file was modified src/HOL/Real_Vector_Spaces.thy (diff)