Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. Some tidying up (mostly regarding summations from 0)
  2. tidied up Infinite_Products
  3. merged
  4. fixed HOL-Analysis
  5. merged; resolved conflicts manually (esp. lemmas that have been moved from Linear_Algebra and Cartesian_Euclidean_Space)
  6. added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
  7. a lemma about infinite products
  8. merged
  9. tidying up and using real induction methods
Changeset 68077:ee8c13ae81e9 by paulson _lp15@cam.ac.uk_:
Some tidying up (mostly regarding summations from 0)
The file was modified src/HOL/Analysis/Cartesian_Euclidean_Space.thy (diff)
The file was modified src/HOL/Analysis/Starlike.thy (diff)
The file was modified src/HOL/Analysis/Weierstrass_Theorems.thy (diff)
The file was modified src/HOL/Analysis/Winding_Numbers.thy (diff)
The file was modified src/HOL/Binomial.thy (diff)
The file was modified src/HOL/NthRoot.thy (diff)
The file was modified src/HOL/Transcendental.thy (diff)
Changeset 68076:315043faa871 by paulson _lp15@cam.ac.uk_:
tidied up Infinite_Products
The file was modified src/HOL/Analysis/Infinite_Products.thy (diff)
Changeset 68075:262b42b59151 by immler:
merged
Changeset 68074:8d50467f7555 by immler:
fixed HOL-Analysis
The file was modified src/HOL/Analysis/Cartesian_Euclidean_Space.thy (diff)
The file was modified src/HOL/Analysis/Cartesian_Space.thy (diff)
The file was modified src/HOL/Analysis/Change_Of_Vars.thy (diff)
The file was modified src/HOL/Analysis/Convex_Euclidean_Space.thy (diff)
The file was modified src/HOL/Analysis/Determinants.thy (diff)
The file was modified src/HOL/Analysis/Finite_Cartesian_Product.thy (diff)
The file was modified src/HOL/Analysis/Homeomorphism.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/Modules.thy (diff)
The file was modified src/HOL/Vector_Spaces.thy (diff)
Changeset 68073:fad29d2a17a5 by immler:
merged; resolved conflicts manually (esp. lemmas that have been moved from Linear_Algebra and Cartesian_Euclidean_Space)
Changeset 68072:493b818e8e10 by immler:
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
The file was addedsrc/HOL/Analysis/Cartesian_Space.thy
The file was addedsrc/HOL/FuncSet.thy
The file was addedsrc/HOL/Hull.thy
The file was addedsrc/HOL/Modules.thy
The file was addedsrc/HOL/Vector_Spaces.thy
The file was modified CONTRIBUTORS (diff)
The file was modified NEWS (diff)
The file was modified src/HOL/Algebra/Congruence.thy (diff)
The file was modified src/HOL/Algebra/Group.thy (diff)
The file was modified src/HOL/Algebra/Order.thy (diff)
The file was modified src/HOL/Analysis/Bochner_Integration.thy (diff)
The file was modified src/HOL/Analysis/Bounded_Linear_Function.thy (diff)
The file was modified src/HOL/Analysis/Cartesian_Euclidean_Space.thy (diff)
The file was modified src/HOL/Analysis/Change_Of_Vars.thy (diff)
The file was modified src/HOL/Analysis/Connected.thy (diff)
The file was modified src/HOL/Analysis/Convex_Euclidean_Space.thy (diff)
The file was modified src/HOL/Analysis/Derivative.thy (diff)
The file was modified src/HOL/Analysis/Determinants.thy (diff)
The file was modified src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy (diff)
The file was modified src/HOL/Analysis/Euclidean_Space.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/Henstock_Kurzweil_Integration.thy (diff)
The file was modified src/HOL/Analysis/Homeomorphism.thy (diff)
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/Analysis/Path_Connected.thy (diff)
The file was modified src/HOL/Analysis/Polytope.thy (diff)
The file was modified src/HOL/Analysis/Product_Vector.thy (diff)
The file was modified src/HOL/Analysis/Sigma_Algebra.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/Analysis/Weierstrass_Theorems.thy (diff)
The file was modified src/HOL/Computational_Algebra/Formal_Power_Series.thy (diff)
The file was modified src/HOL/HOL.thy (diff)
The file was modified src/HOL/Library/Library.thy (diff)
The file was modified src/HOL/Metis_Examples/Abstraction.thy (diff)
The file was modified src/HOL/Metis_Examples/Tarski.thy (diff)
The file was modified src/HOL/Number_Theory/Prime_Powers.thy (diff)
The file was modified src/HOL/Real_Vector_Spaces.thy (diff)
The file was modified src/HOL/ex/Ballot.thy (diff)
The file was modified src/HOL/ex/Birthday_Paradox.thy (diff)
The file was modified src/HOL/ex/Tarski.thy (diff)
The file was removedsrc/HOL/Library/FuncSet.thy
Changeset 68071:c18af2b0f83e by paulson _lp15@cam.ac.uk_:
a lemma about infinite products
The file was modified src/HOL/Analysis/Infinite_Products.thy (diff)
Changeset 68070:8dc792d440b9 by paulson:
merged
Changeset 68069:36209dfb981e by paulson _lp15@cam.ac.uk_:
tidying up and using real induction methods
The file was modified src/HOL/Analysis/Cartesian_Euclidean_Space.thy (diff)
The file was modified src/HOL/Analysis/Change_Of_Vars.thy (diff)
The file was modified src/HOL/Analysis/Convex_Euclidean_Space.thy (diff)
The file was modified src/HOL/Analysis/Determinants.thy (diff)
The file was modified src/HOL/Analysis/Homeomorphism.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)