Changes

Summary

merged
renamed listsum -> sum_list, listprod ~> prod_list
lots of new results about topology, affine dimension etc

Changeset 63883:41b5d9f3778a by nipkow: merged
Changeset 63882:018998c00003 by nipkow: renamed listsum -> sum_list, listprod ~> prod_list
The file was modified	`NEWS` (diff)
The file was modified	`src/HOL/Binomial.thy` (diff)
The file was modified	`src/HOL/GCD.thy` (diff)
The file was modified	`src/HOL/Groups_List.thy` (diff)
The file was modified	`src/HOL/IMP/Abs_Int0.thy` (diff)
The file was modified	`src/HOL/IMP/Abs_Int1.thy` (diff)
The file was modified	`src/HOL/IMP/Abs_Int3.thy` (diff)
The file was modified	`src/HOL/Library/Extended_Nonnegative_Real.thy` (diff)
The file was modified	`src/HOL/Library/Extended_Real.thy` (diff)
The file was modified	`src/HOL/Library/Formal_Power_Series.thy` (diff)
The file was modified	`src/HOL/Library/ListVector.thy` (diff)
The file was modified	`src/HOL/Library/Multiset.thy` (diff)
The file was modified	`src/HOL/Library/Polynomial.thy` (diff)
The file was modified	`src/HOL/Library/Polynomial_FPS.thy` (diff)
The file was modified	`src/HOL/Nitpick.thy` (diff)
The file was modified	`src/HOL/Nominal/Examples/Standardization.thy` (diff)
The file was modified	`src/HOL/Predicate_Compile_Examples/Predicate_Compile_Quickcheck_Examples.thy` (diff)
The file was modified	`src/HOL/Probability/PMF_Impl.thy` (diff)
The file was modified	`src/HOL/Probability/Probability_Mass_Function.thy` (diff)
The file was modified	`src/HOL/Proofs/Lambda/ListApplication.thy` (diff)
The file was modified	`src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy` (diff)
The file was modified	`src/HOL/Random.thy` (diff)
The file was modified	`src/HOL/UNITY/Comp/AllocBase.thy` (diff)
The file was modified	`src/HOL/ex/Gauge_Integration.thy` (diff)
The file was modified	`src/HOL/ex/Parallel_Example.thy` (diff)
The file was modified	`src/HOL/ex/Perm_Fragments.thy` (diff)
The file was modified	`src/HOL/ex/Primrec.thy` (diff)
The file was modified	`src/HOL/ex/Transfer_Int_Nat.thy` (diff)
Changeset 63881:b746b19197bd by paulson _lp15@cam.ac.uk_: lots of new results about topology, affine dimension etc
The file was modified	`src/HOL/Analysis/Convex_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/Topology_Euclidean_Space.thy` (diff)
The file was modified	`src/HOL/Library/Continuum_Not_Denumerable.thy` (diff)