Skip to content
[Jenkins]Jenkins
log in
Failed

Changes

Summary

  1. merged
  2. updated to setsum -> sum
  3. setsum -> sum
Changeset 64269:c939cc16b605 by nipkow:
merged
Changeset 64268:3faa948dc861 by nipkow:
updated to setsum -> sum
The file was modified src/Doc/Prog_Prove/Bool_nat_list.thy (diff)
Changeset 64267:b9a1486e79be by nipkow:
setsum -> sum
The file was modified src/Doc/Logics/document/HOL.tex (diff)
The file was modified src/Doc/Main/Main_Doc.thy (diff)
The file was modified src/Doc/Sugar/Sugar.thy (diff)
The file was modified src/HOL/Algebra/IntRing.thy (diff)
The file was modified src/HOL/Analysis/Binary_Product_Measure.thy (diff)
The file was modified src/HOL/Analysis/Bochner_Integration.thy (diff)
The file was modified src/HOL/Analysis/Borel_Space.thy (diff)
The file was modified src/HOL/Analysis/Bounded_Continuous_Function.thy (diff)
The file was modified src/HOL/Analysis/Bounded_Linear_Function.thy (diff)
The file was modified src/HOL/Analysis/Brouwer_Fixpoint.thy (diff)
The file was modified src/HOL/Analysis/Caratheodory.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/Continuous_Extension.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/Fashoda_Theorem.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/Harmonic_Numbers.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/Integral_Test.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/Measure_Space.thy (diff)
The file was modified src/HOL/Analysis/Nonnegative_Lebesgue_Integration.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/Regularity.thy (diff)
The file was modified src/HOL/Analysis/Summation_Tests.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/Uniform_Limit.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/Complex.thy (diff)
The file was modified src/HOL/Datatype_Examples/Misc_Primrec.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/Groups_List.thy (diff)
The file was modified src/HOL/HOLCF/Universal.thy (diff)
The file was modified src/HOL/Hoare_Parallel/OG_Examples.thy (diff)
The file was modified src/HOL/Hoare_Parallel/RG_Examples.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/IMP/Abs_Int_ITP/Abs_Int1_ITP.thy (diff)
The file was modified src/HOL/IMP/Abs_Int_ITP/Abs_Int3_ITP.thy (diff)
The file was modified src/HOL/Inequalities.thy (diff)
The file was modified src/HOL/Int.thy (diff)
The file was modified src/HOL/Library/BigO.thy (diff)
The file was modified src/HOL/Library/Bourbaki_Witt_Fixpoint.thy (diff)
The file was modified src/HOL/Library/Combine_PER.thy (diff)
The file was modified src/HOL/Library/Extended_Nat.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/FSet.thy (diff)
The file was modified src/HOL/Library/Finite_Map.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/Indicator_Function.thy (diff)
The file was modified src/HOL/Library/Multiset.thy (diff)
The file was modified src/HOL/Library/Multiset_Permutations.thy (diff)
The file was modified src/HOL/Library/Nat_Bijection.thy (diff)
The file was modified src/HOL/Library/Permutations.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/Library/Polynomial_Factorial.thy (diff)
The file was modified src/HOL/Library/Product_Plus.thy (diff)
The file was modified src/HOL/Library/RBT_Set.thy (diff)
The file was modified src/HOL/Library/Set_Algebras.thy (diff)
The file was modified src/HOL/Library/Stirling.thy (diff)
The file was modified src/HOL/Lifting_Set.thy (diff)
The file was modified src/HOL/Limits.thy (diff)
The file was modified src/HOL/List.thy (diff)
The file was modified src/HOL/MacLaurin.thy (diff)
The file was modified src/HOL/Metis_Examples/Big_O.thy (diff)
The file was modified src/HOL/Nat_Transfer.thy (diff)
The file was modified src/HOL/Nitpick.thy (diff)
The file was modified src/HOL/Nonstandard_Analysis/HSeries.thy (diff)
The file was modified src/HOL/Nonstandard_Analysis/Nonstandard_Analysis.thy (diff)
The file was modified src/HOL/NthRoot.thy (diff)
The file was modified src/HOL/Number_Theory/Cong.thy (diff)
The file was modified src/HOL/Number_Theory/Factorial_Ring.thy (diff)
The file was modified src/HOL/Number_Theory/Fib.thy (diff)
The file was modified src/HOL/Old_Number_Theory/Euler.thy (diff)
The file was modified src/HOL/Old_Number_Theory/Fib.thy (diff)
The file was modified src/HOL/Old_Number_Theory/Finite2.thy (diff)
The file was modified src/HOL/Old_Number_Theory/Quadratic_Reciprocity.thy (diff)
The file was modified src/HOL/Old_Number_Theory/Residues.thy (diff)
The file was modified src/HOL/Predicate_Compile_Examples/Predicate_Compile_Quickcheck_Examples.thy (diff)
The file was modified src/HOL/Probability/Central_Limit_Theorem.thy (diff)
The file was modified src/HOL/Probability/Characteristic_Functions.thy (diff)
The file was modified src/HOL/Probability/Distributions.thy (diff)
The file was modified src/HOL/Probability/Independent_Family.thy (diff)
The file was modified src/HOL/Probability/Information.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/Probability/Probability_Measure.thy (diff)
The file was modified src/HOL/Probability/Projective_Limit.thy (diff)
The file was modified src/HOL/Probability/SPMF.thy (diff)
The file was modified src/HOL/Probability/ex/Koepf_Duermuth_Countermeasure.thy (diff)
The file was modified src/HOL/Rat.thy (diff)
The file was modified src/HOL/Real.thy (diff)
The file was modified src/HOL/Real_Vector_Spaces.thy (diff)
The file was modified src/HOL/Series.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/UNITY/Comp/Alloc.thy (diff)
The file was modified src/HOL/UNITY/Comp/AllocBase.thy (diff)
The file was modified src/HOL/UNITY/Comp/AllocImpl.thy (diff)
The file was modified src/HOL/UNITY/Follows.thy (diff)
The file was modified src/HOL/ex/Execute_Choice.thy (diff)
The file was modified src/HOL/ex/HarmonicSeries.thy (diff)
The file was modified src/HOL/ex/Meson_Test.thy (diff)
The file was modified src/HOL/ex/Sum_of_Powers.thy (diff)
The file was modified src/HOL/ex/ThreeDivides.thy (diff)
The file was modified src/HOL/ex/Transfer_Int_Nat.thy (diff)