Skip to content
[Jenkins]Jenkins
log in
Failed

Changes

Summary

  1. merged
  2. fixed HOL-Analysis
  3. merged; resolved conflicts manually (esp. lemmas that have been moved from Linear_Algebra and Cartesian_Euclidean_Space)
  4. added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
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