Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. most of Topology_Euclidean_Space (now Elementary_Topology) requires fewer dependencies
  2. merged
  3. tuned headers
  4. moved lemmas up
  5. prove lemmas in context real_normed_vector
  6. moved dependency
  7. generalized to big sum
  8. merged
  9. tuned headers; ~ -> \<not>
  10. update LTS Haskell version
Changeset 69516:09bb8f470959 by immler:
most of Topology_Euclidean_Space (now Elementary_Topology) requires fewer dependencies
The file was addedsrc/HOL/Analysis/Elementary_Topology.thy
The file was modified src/HOL/Analysis/Conformal_Mappings.thy (diff)
The file was modified src/HOL/Analysis/Euclidean_Space.thy (diff)
The file was modified src/HOL/Analysis/Linear_Algebra.thy (diff)
The file was modified src/HOL/Analysis/Path_Connected.thy (diff)
The file was modified src/HOL/Analysis/Starlike.thy (diff)
The file was modified src/HOL/Analysis/Topology_Euclidean_Space.thy (diff)
The file was modified src/HOL/Library/Infinite_Set.thy (diff)
Changeset 69515:5bbb2bd564fa by nipkow:
merged
Changeset 69514:58a77f548bb6 by nipkow:
tuned headers
The file was modified src/HOL/Analysis/Path_Connected.thy (diff)
Changeset 69513:42e08052dae8 by immler:
moved lemmas up
The file was modified src/HOL/Analysis/Inner_Product.thy (diff)
The file was modified src/HOL/Analysis/Linear_Algebra.thy (diff)
The file was modified src/HOL/Real_Vector_Spaces.thy (diff)
Changeset 69512:2b54f25e66c4 by immler:
prove lemmas in context real_normed_vector
The file was modified src/HOL/Real_Vector_Spaces.thy (diff)
Changeset 69511:4cc5e4a528f8 by immler:
moved dependency
The file was modified src/HOL/Analysis/Euclidean_Space.thy (diff)
The file was modified src/HOL/Analysis/Product_Vector.thy (diff)
Changeset 69510:0f31dd2e540d by immler:
generalized to big sum
The file was modified src/HOL/Analysis/Convex_Euclidean_Space.thy (diff)
The file was modified src/HOL/Analysis/Henstock_Kurzweil_Integration.thy (diff)
The file was modified src/HOL/Analysis/Linear_Algebra.thy (diff)
The file was modified src/HOL/Groups_Big.thy (diff)
Changeset 69509:f9bf65d90b69 by nipkow:
merged
Changeset 69508:2a4c8a2a3f8e by nipkow:
tuned headers; ~ -&gt; \&lt;not&gt;
The file was modified src/HOL/Analysis/Abstract_Topology.thy (diff)
The file was modified src/HOL/Analysis/Brouwer_Fixpoint.thy (diff)
The file was modified src/HOL/Analysis/Cartesian_Euclidean_Space.thy (diff)
The file was modified src/HOL/Analysis/Cauchy_Integral_Theorem.thy (diff)
The file was modified src/HOL/Analysis/Complex_Analysis_Basics.thy (diff)
The file was modified src/HOL/Analysis/Complex_Transcendental.thy (diff)
The file was modified src/HOL/Analysis/Conformal_Mappings.thy (diff)
The file was modified src/HOL/Analysis/Connected.thy (diff)
The file was modified src/HOL/Analysis/Continuous_Extension.thy (diff)
The file was modified src/HOL/Analysis/Convex_Euclidean_Space.thy (diff)
The file was modified src/HOL/Analysis/Cross3.thy (diff)
The file was modified src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy (diff)
The file was modified src/HOL/Analysis/Further_Topology.thy (diff)
The file was modified src/HOL/Analysis/Great_Picard.thy (diff)
The file was modified src/HOL/Analysis/Henstock_Kurzweil_Integration.thy (diff)
The file was modified src/HOL/Analysis/Homeomorphism.thy (diff)
The file was modified src/HOL/Analysis/Improper_Integral.thy (diff)
The file was modified src/HOL/Analysis/Jordan_Curve.thy (diff)
The file was modified src/HOL/Analysis/Ordered_Euclidean_Space.thy (diff)
The file was modified src/HOL/Analysis/Path_Connected.thy (diff)
The file was modified src/HOL/Analysis/Poly_Roots.thy (diff)
The file was modified src/HOL/Analysis/Polytope.thy (diff)
The file was modified src/HOL/Analysis/Riemann_Mapping.thy (diff)
The file was modified src/HOL/Analysis/Starlike.thy (diff)
The file was modified src/HOL/Analysis/Tagged_Division.thy (diff)
The file was modified src/HOL/Analysis/Topology_Euclidean_Space.thy (diff)
The file was modified src/HOL/Analysis/Weierstrass_Theorems.thy (diff)
The file was modified src/HOL/Analysis/Winding_Numbers.thy (diff)
Changeset 69507:04e54f57a869 by lars hupel _lars.hupel@mytum.de_:
update LTS Haskell version
The file was modified etc/settings (diff)
The file was modified src/Pure/General/path.ML (diff)