Skip to content
Success

Changes

Summary

  1. Tuned some proofs in HOL-Analysis
  2. The Uniq quantifier for FOL too
Changeset 71840:8ed78bb0b915 by manuel eberl _eberlm@in.tum.de_:
Tuned some proofs in HOL-Analysis
The file was modified src/HOL/Analysis/Abstract_Topology.thy (diff)
The file was modified src/HOL/Analysis/Affine.thy (diff)
The file was modified src/HOL/Analysis/Bochner_Integration.thy (diff)
The file was modified src/HOL/Analysis/Finite_Cartesian_Product.thy (diff)
The file was modified src/HOL/Analysis/Further_Topology.thy (diff)
The file was modified src/HOL/Analysis/Measure_Space.thy (diff)
The file was modified src/HOL/Analysis/Polytope.thy (diff)
The file was modified src/HOL/Library/Infinite_Set.thy (diff)
Changeset 71839:0bbe0866b7e6 by paulson _lp15@cam.ac.uk_:
The Uniq quantifier for FOL too
The file was modified NEWS (diff)
The file was modified src/FOL/IFOL.thy (diff)