Changes

Summary

# after multiset intersection and union symbol
left_distrib ~> distrib_right, right_distrib ~> distrib_left

Changeset 63919:9aed2da07200 by fleury _mathias.fleury@mpi-inf.mpg.de_: # after multiset intersection and union symbol
The file was modified	`NEWS` (diff)
The file was modified	`src/HOL/Algebra/Divisibility.thy` (diff)
The file was modified	`src/HOL/Library/Multiset.thy` (diff)
The file was modified	`src/HOL/Number_Theory/Factorial_Ring.thy` (diff)
Changeset 63918:6bf55e6e0b75 by fleury _mathias.fleury@mpi-inf.mpg.de_: left_distrib ~> distrib_right, right_distrib ~> distrib_left
The file was modified	`NEWS` (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/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/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/Finite_Cartesian_Product.thy` (diff)
The file was modified	`src/HOL/Analysis/Gamma_Function.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/L2_Norm.thy` (diff)
The file was modified	`src/HOL/Analysis/Lebesgue_Measure.thy` (diff)
The file was modified	`src/HOL/Analysis/Linear_Algebra.thy` (diff)
The file was modified	`src/HOL/Analysis/Nonnegative_Lebesgue_Integration.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/Summation_Tests.thy` (diff)
The file was modified	`src/HOL/Analysis/Weierstrass_Theorems.thy` (diff)
The file was modified	`src/HOL/Analysis/ex/Approximations.thy` (diff)
The file was modified	`src/HOL/Binomial.thy` (diff)
The file was modified	`src/HOL/Decision_Procs/Approximation.thy` (diff)
The file was modified	`src/HOL/Deriv.thy` (diff)
The file was modified	`src/HOL/Groups_Big.thy` (diff)
The file was modified	`src/HOL/Inequalities.thy` (diff)
The file was modified	`src/HOL/Library/BigO.thy` (diff)
The file was modified	`src/HOL/Library/Convex.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/Groups_Big_Fun.thy` (diff)
The file was modified	`src/HOL/Library/Polynomial.thy` (diff)
The file was modified	`src/HOL/Library/Stirling.thy` (diff)
The file was modified	`src/HOL/Metis_Examples/Big_O.thy` (diff)
The file was modified	`src/HOL/Nonstandard_Analysis/HSeries.thy` (diff)
The file was modified	`src/HOL/Probability/Distributions.thy` (diff)
The file was modified	`src/HOL/Probability/Probability_Mass_Function.thy` (diff)
The file was modified	`src/HOL/Probability/Projective_Limit.thy` (diff)
The file was modified	`src/HOL/Probability/ex/Koepf_Duermuth_Countermeasure.thy` (diff)
The file was modified	`src/HOL/Set_Interval.thy` (diff)
The file was modified	`src/HOL/Transcendental.thy` (diff)
The file was modified	`src/HOL/ex/Sum_of_Powers.thy` (diff)
The file was modified	`src/HOL/ex/ThreeDivides.thy` (diff)