Changes

Summary

setsum -> sum

Changeset 7209:19b03dc6b859 by nipkow: setsum -> sum
The file was modified	`thys/Affine_Arithmetic/Affine_Approximation.thy` (diff)
The file was modified	`thys/Affine_Arithmetic/Affine_Code.thy` (diff)
The file was modified	`thys/Affine_Arithmetic/Affine_Form.thy` (diff)
The file was modified	`thys/Affine_Arithmetic/Counterclockwise.thy` (diff)
The file was modified	`thys/Affine_Arithmetic/Counterclockwise_2D_Arbitrary.thy` (diff)
The file was modified	`thys/Affine_Arithmetic/Counterclockwise_2D_Strict.thy` (diff)
The file was modified	`thys/Affine_Arithmetic/Counterclockwise_Vector.thy` (diff)
The file was modified	`thys/Affine_Arithmetic/Euclidean_Space_Explicit.thy` (diff)
The file was modified	`thys/Affine_Arithmetic/Executable_Euclidean_Space.thy` (diff)
The file was modified	`thys/Affine_Arithmetic/Intersection.thy` (diff)
The file was modified	`thys/Affine_Arithmetic/Polygon.thy` (diff)
The file was modified	`thys/Akra_Bazzi/Akra_Bazzi.thy` (diff)
The file was modified	`thys/Akra_Bazzi/Akra_Bazzi_Approximation.thy` (diff)
The file was modified	`thys/Akra_Bazzi/Akra_Bazzi_Library.thy` (diff)
The file was modified	`thys/Akra_Bazzi/Akra_Bazzi_Method.thy` (diff)
The file was modified	`thys/Akra_Bazzi/Akra_Bazzi_Real.thy` (diff)
The file was modified	`thys/Akra_Bazzi/Master_Theorem.thy` (diff)
The file was modified	`thys/Akra_Bazzi/akra_bazzi.ML` (diff)
The file was modified	`thys/Akra_Bazzi/akra_bazzi_approximation.ML` (diff)
The file was modified	`thys/Algebraic_Numbers/Algebraic_Numbers.thy` (diff)
The file was modified	`thys/Algebraic_Numbers/Algebraic_Numbers_Prelim.thy` (diff)
The file was modified	`thys/Algebraic_Numbers/Bivariate_Polynomials.thy` (diff)
The file was modified	`thys/Algebraic_Numbers/Complex_Roots_Real_Poly.thy` (diff)
The file was modified	`thys/Algebraic_Numbers/Real_Roots.thy` (diff)
The file was modified	`thys/Algebraic_Numbers/Resultant.thy` (diff)
The file was modified	`thys/Amortized_Complexity/Amortized_Framework0.thy` (diff)
The file was modified	`thys/Automatic_Refinement/Lib/Misc.thy` (diff)
The file was modified	`thys/Bell_Numbers_Spivey/Bell_Numbers.thy` (diff)
The file was modified	`thys/Berlekamp_Zassenhaus/Berlekamp_Type_Based.thy` (diff)
The file was modified	`thys/Berlekamp_Zassenhaus/Chinese_Remainder_Poly.thy` (diff)
The file was modified	`thys/Berlekamp_Zassenhaus/Factor_Bound.thy` (diff)
The file was modified	`thys/Berlekamp_Zassenhaus/Hensel_Lifting_Type_Based.thy` (diff)
The file was modified	`thys/Berlekamp_Zassenhaus/Poly_Mod.thy` (diff)
The file was modified	`thys/Card_Equiv_Relations/Card_Equiv_Relations.thy` (diff)
The file was modified	`thys/Card_Equiv_Relations/Card_Partial_Equiv_Relations.thy` (diff)
The file was modified	`thys/Card_Number_Partitions/Additions_to_Main.thy` (diff)
The file was modified	`thys/Card_Number_Partitions/Card_Number_Partitions.thy` (diff)
The file was modified	`thys/Card_Number_Partitions/Number_Partition.thy` (diff)
The file was modified	`thys/Cartan_FP/Cartan.thy` (diff)
The file was modified	`thys/Catalan_Numbers/Catalan_Numbers.thy` (diff)
The file was modified	`thys/Cauchy/CauchySchwarz.thy` (diff)
The file was modified	`thys/Cayley_Hamilton/Cayley_Hamilton.thy` (diff)
The file was modified	`thys/Cayley_Hamilton/Square_Matrix.thy` (diff)
The file was modified	`thys/ClockSynchInst/ICAInstance.thy` (diff)
The file was modified	`thys/Coinductive/Coinductive_List.thy` (diff)
The file was modified	`thys/Coinductive/Examples/LList_CCPO_Topology.thy` (diff)
The file was modified	`thys/Containers/Set_Impl.thy` (diff)
The file was modified	`thys/Descartes_Sign_Rule/Descartes_Sign_Rule.thy` (diff)
The file was modified	`thys/Discrete_Summation/Discrete_Summation.thy` (diff)
The file was modified	`thys/Discrete_Summation/Factorials.thy` (diff)
The file was modified	`thys/Echelon_Form/Code_Cayley_Hamilton.thy` (diff)
The file was modified	`thys/Echelon_Form/Echelon_Form.thy` (diff)
The file was modified	`thys/Echelon_Form/Echelon_Form_Inverse.thy` (diff)
The file was modified	`thys/Echelon_Form/Rings2.thy` (diff)
The file was modified	`thys/EdmondsKarp_Maxflow/Augmenting_Flow.thy` (diff)
The file was modified	`thys/EdmondsKarp_Maxflow/Augmenting_Path.thy` (diff)
The file was modified	`thys/EdmondsKarp_Maxflow/Edka_Checked_Impl.thy` (diff)
The file was modified	`thys/EdmondsKarp_Maxflow/Ford_Fulkerson.thy` (diff)
The file was modified	`thys/EdmondsKarp_Maxflow/Graph.thy` (diff)
The file was modified	`thys/EdmondsKarp_Maxflow/Refine_Add_Fofu.thy` (diff)
The file was modified	`thys/Ergodic_Theory/Conditional_Expectation.thy` (diff)
The file was modified	`thys/Ergodic_Theory/Gouezel_Karlsson.thy` (diff)
The file was modified	`thys/Ergodic_Theory/Invariants.thy` (diff)
The file was modified	`thys/Ergodic_Theory/Kingman.thy` (diff)
The file was modified	`thys/Ergodic_Theory/Measure_Preserving_Transformations.thy` (diff)
The file was modified	`thys/Ergodic_Theory/Product_Topology.thy` (diff)
The file was modified	`thys/Ergodic_Theory/Recurrence.thy` (diff)
The file was modified	`thys/Ergodic_Theory/SG_Library_Complement.thy` (diff)
The file was modified	`thys/Euler_Partition/Euler_Partition.thy` (diff)
The file was modified	`thys/FFT/FFT.thy` (diff)
The file was modified	`thys/Fisher_Yates/Fisher_Yates.thy` (diff)
The file was modified	`thys/Flyspeck-Tame/GeneratorProps.thy` (diff)
The file was modified	`thys/Flyspeck-Tame/ListSum.thy` (diff)
The file was modified	`thys/Flyspeck-Tame/LowerBound.thy` (diff)
The file was modified	`thys/Flyspeck-Tame/ScoreProps.thy` (diff)
The file was modified	`thys/Formula_Derivatives/WS1S_Formula.thy` (diff)
The file was modified	`thys/Gauss-Jordan-Elim-Fun/Gauss_Jordan_Elim_Fun.thy` (diff)
The file was modified	`thys/Gauss_Jordan/Code_Matrix.thy` (diff)
The file was modified	`thys/Gauss_Jordan/Elementary_Operations.thy` (diff)
The file was modified	`thys/Gauss_Jordan/Gauss_Jordan.thy` (diff)
The file was modified	`thys/Gauss_Jordan/Gauss_Jordan_PA.thy` (diff)
The file was modified	`thys/Gauss_Jordan/Inverse.thy` (diff)
The file was modified	`thys/Gauss_Jordan/Linear_Maps.thy` (diff)
The file was modified	`thys/Gauss_Jordan/Matrix_To_IArray.thy` (diff)
The file was modified	`thys/Gauss_Jordan/System_Of_Equations.thy` (diff)
The file was modified	`thys/Girth_Chromatic/Girth_Chromatic.thy` (diff)
The file was modified	`thys/Girth_Chromatic/Ugraphs.thy` (diff)
The file was modified	`thys/Graph_Theory/Bidirected_Digraph.thy` (diff)
The file was modified	`thys/Hermite/Hermite.thy` (diff)
The file was modified	`thys/Huffman/Huffman.thy` (diff)
The file was modified	`thys/Integration/Failure.thy` (diff)
The file was modified	`thys/Integration/Integral.thy` (diff)
The file was modified	`thys/JinjaThreads/Basic/Auxiliary.thy` (diff)
The file was modified	`thys/JinjaThreads/Framework/LTS.thy` (diff)
The file was modified	`thys/JinjaThreads/MM/JMM_Framework.thy` (diff)
The file was modified	`thys/JinjaThreads/MM/JMM_Typesafe.thy` (diff)
The file was modified	`thys/Jordan_Normal_Form/Char_Poly.thy` (diff)
The file was modified	`thys/Jordan_Normal_Form/Conjugate.thy` (diff)
The file was modified	`thys/Jordan_Normal_Form/Determinant.thy` (diff)
The file was modified	`thys/Jordan_Normal_Form/Gauss_Jordan_Elimination.thy` (diff)
The file was modified	`thys/Jordan_Normal_Form/Gram_Schmidt.thy` (diff)
The file was modified	`thys/Jordan_Normal_Form/Jordan_Normal_Form.thy` (diff)
The file was modified	`thys/Jordan_Normal_Form/Matrix.thy` (diff)
The file was modified	`thys/Jordan_Normal_Form/Matrix_Comparison.thy` (diff)
The file was modified	`thys/Jordan_Normal_Form/Matrix_Kernel.thy` (diff)
The file was modified	`thys/Jordan_Normal_Form/Missing_Permutations.thy` (diff)
The file was modified	`thys/Jordan_Normal_Form/Missing_VectorSpace.thy` (diff)
The file was modified	`thys/Jordan_Normal_Form/Schur_Decomposition.thy` (diff)
The file was modified	`thys/Jordan_Normal_Form/VS_Connect.thy` (diff)
The file was modified	`thys/Kleene_Algebra/Finite_Suprema.thy` (diff)
The file was modified	`thys/Kleene_Algebra/Formal_Power_Series.thy` (diff)
The file was modified	`thys/Kleene_Algebra/Inf_Matrix.thy` (diff)
The file was modified	`thys/Kleene_Algebra/Matrix.thy` (diff)
The file was modified	`thys/LTL/LTL.thy` (diff)
The file was modified	`thys/LTL_to_GBA/LTL_to_GBA.thy` (diff)
The file was modified	`thys/Lehmer/Multiplicative_Group.thy` (diff)
The file was modified	`thys/Liouville_Numbers/Liouville_Numbers.thy` (diff)
The file was modified	`thys/Liouville_Numbers/Liouville_Numbers_Misc.thy` (diff)
The file was modified	`thys/List-Infinite/CommonSet/SetInterval2.thy` (diff)
The file was modified	`thys/List_Update/BIT.thy` (diff)
The file was modified	`thys/List_Update/BIT_2comp_on2.thy` (diff)
The file was modified	`thys/List_Update/Bit_Strings.thy` (diff)
The file was modified	`thys/List_Update/Competitive_Analysis.thy` (diff)
The file was modified	`thys/List_Update/List_Factoring.thy` (diff)
The file was modified	`thys/List_Update/Move_to_Front.thy` (diff)
The file was modified	`thys/List_Update/On_Off.thy` (diff)
The file was modified	`thys/List_Update/Phase_Partitioning.thy` (diff)
The file was modified	`thys/List_Update/Prob_Theory.thy` (diff)
The file was modified	`thys/Lower_Semicontinuous/Lower_Semicontinuous.thy` (diff)
The file was modified	`thys/Lp/Functional_Spaces.thy` (diff)
The file was modified	`thys/Lp/Lp.thy` (diff)
The file was modified	`thys/MFMC_Countable/Max_Flow_Min_Cut_Countable.thy` (diff)
The file was modified	`thys/Markov_Models/Classifying_Markov_Chain_States.thy` (diff)
The file was modified	`thys/Markov_Models/Continuous_Time_Markov_Chain.thy` (diff)
The file was modified	`thys/Markov_Models/ex/Crowds_Protocol.thy` (diff)
The file was modified	`thys/Markov_Models/ex/Gossip_Broadcast.thy` (diff)
The file was modified	`thys/Markov_Models/ex/MDP_RP_Certification.thy` (diff)
The file was modified	`thys/Markov_Models/ex/PCTL.thy` (diff)
The file was modified	`thys/Marriage/Marriage.thy` (diff)
The file was modified	`thys/Max-Card-Matching/Matching.thy` (diff)
The file was modified	`thys/Multivariate_Polynomials/Poly_Lists.thy` (diff)
The file was modified	`thys/Multivariate_Polynomials/Power_Products.thy` (diff)
The file was modified	`thys/Nat-Interval-Logic/IL_IntervalOperators.thy` (diff)
The file was modified	`thys/Ordinary_Differential_Equations/IVP/Flow.thy` (diff)
The file was modified	`thys/Ordinary_Differential_Equations/IVP/Initial_Value_Problem.thy` (diff)
The file was modified	`thys/Ordinary_Differential_Equations/IVP/Picard_Lindeloef_Qualitative.thy` (diff)
The file was modified	`thys/Ordinary_Differential_Equations/Numerics/Refine_Reachability_Analysis.thy` (diff)
The file was modified	`thys/Ordinary_Differential_Equations/Numerics/Runge_Kutta.thy` (diff)
The file was modified	`thys/Ordinary_Differential_Equations/ODE_Auxiliarities.thy` (diff)
The file was modified	`thys/Perfect-Number-Thm/PerfectBasics.thy` (diff)
The file was modified	`thys/Perfect-Number-Thm/Sigma.thy` (diff)
The file was modified	`thys/Perron_Frobenius/HMA_Connect.thy` (diff)
The file was modified	`thys/Perron_Frobenius/Perron_Frobenius.thy` (diff)
The file was modified	`thys/Polynomial_Factorization/Gauss_Lemma.thy` (diff)
The file was modified	`thys/Polynomial_Factorization/Order_Polynomial.thy` (diff)
The file was modified	`thys/Polynomial_Factorization/Square_Free_Factorization.thy` (diff)
The file was modified	`thys/Polynomial_Interpolation/Missing_Polynomial.thy` (diff)
The file was modified	`thys/Polynomial_Interpolation/Newton_Interpolation.thy` (diff)
The file was modified	`thys/Polynomial_Interpolation/Ring_Hom.thy` (diff)
The file was modified	`thys/Polynomial_Interpolation/Ring_Hom_Poly.thy` (diff)
The file was modified	`thys/Prime_Harmonic_Series/Prime_Harmonic.thy` (diff)
The file was modified	`thys/Prime_Harmonic_Series/Prime_Harmonic_Misc.thy` (diff)
The file was modified	`thys/Probabilistic_Noninterference/Compositionality.thy` (diff)
The file was modified	`thys/Probabilistic_Noninterference/Language_Semantics.thy` (diff)
The file was modified	`thys/Probabilistic_Noninterference/Resumption_Based.thy` (diff)
The file was modified	`thys/Probabilistic_Noninterference/Trace_Based.thy` (diff)
The file was modified	`thys/Program-Conflict-Analysis/Misc.thy` (diff)
The file was modified	`thys/QR_Decomposition/Generalizations2.thy` (diff)
The file was modified	`thys/QR_Decomposition/Gram_Schmidt.thy` (diff)
The file was modified	`thys/QR_Decomposition/Gram_Schmidt_IArrays.thy` (diff)
The file was modified	`thys/QR_Decomposition/IArray_Addenda_QR.thy` (diff)
The file was modified	`thys/QR_Decomposition/Least_Squares_Approximation.thy` (diff)
The file was modified	`thys/QR_Decomposition/Matrix_To_IArray_QR.thy` (diff)
The file was modified	`thys/QR_Decomposition/Miscellaneous_QR.thy` (diff)
The file was modified	`thys/QR_Decomposition/Projections.thy` (diff)
The file was modified	`thys/QR_Decomposition/QR_Decomposition.thy` (diff)
The file was modified	`thys/QR_Decomposition/QR_Efficient.thy` (diff)
The file was modified	`thys/Random_Graph_Subgraph_Threshold/Prob_Lemmas.thy` (diff)
The file was modified	`thys/Random_Graph_Subgraph_Threshold/Subgraph_Threshold.thy` (diff)
The file was modified	`thys/Random_Graph_Subgraph_Threshold/Ugraph_Misc.thy` (diff)
The file was modified	`thys/Randomised_Social_Choice/Automation/SDS_Automation.thy` (diff)
The file was modified	`thys/Randomised_Social_Choice/Random_Dictatorship.thy` (diff)
The file was modified	`thys/Randomised_Social_Choice/SD_Efficiency.thy` (diff)
The file was modified	`thys/Randomised_Social_Choice/Stochastic_Dominance.thy` (diff)
The file was modified	`thys/Randomised_Social_Choice/Utility_Functions.thy` (diff)
The file was modified	`thys/Rank_Nullity_Theorem/Dim_Formula.thy` (diff)
The file was modified	`thys/Rank_Nullity_Theorem/Fundamental_Subspaces.thy` (diff)
The file was modified	`thys/Rank_Nullity_Theorem/Generalizations.thy` (diff)
The file was modified	`thys/Rank_Nullity_Theorem/Miscellaneous.thy` (diff)
The file was modified	`thys/Recursion-Theory-I/PRecFinSet.thy` (diff)
The file was modified	`thys/Regular_Algebras/Dioid_Power_Sum.thy` (diff)
The file was modified	`thys/Regular_Algebras/Regular_Algebras.thy` (diff)
The file was modified	`thys/Relation_Algebra/Relation_Algebra_Models.thy` (diff)
The file was modified	`thys/Rep_Fin_Groups/Rep_Fin_Groups.thy` (diff)
The file was modified	`thys/Secondary_Sylow/GroupAction.thy` (diff)
The file was modified	`thys/Slicing/JinjaVM/JVMPostdomination.thy` (diff)
The file was modified	`thys/Stirling_Formula/Stirling_Formula.thy` (diff)
The file was modified	`thys/Sturm_Sequences/Lib/Misc_Polynomial.thy` (diff)
The file was modified	`thys/Sturm_Tarski/PolyMisc.thy` (diff)
The file was modified	`thys/Sturm_Tarski/Sturm_Tarski.thy` (diff)
The file was modified	`thys/Tarskis_Geometry/Hyperbolic_Tarski.thy` (diff)
The file was modified	`thys/Tarskis_Geometry/Linear_Algebra2.thy` (diff)
The file was modified	`thys/Tarskis_Geometry/Miscellany.thy` (diff)
The file was modified	`thys/Tarskis_Geometry/Projective.thy` (diff)
The file was modified	`thys/UpDown_Scheme/Down.thy` (diff)
The file was modified	`thys/UpDown_Scheme/Grid.thy` (diff)
The file was modified	`thys/UpDown_Scheme/Grid_Point.thy` (diff)
The file was modified	`thys/UpDown_Scheme/Up.thy` (diff)
The file was modified	`thys/UpDown_Scheme/Up_Down.thy` (diff)
The file was modified	`thys/Vickrey_Clarke_Groves/CombinatorialAuction.thy` (diff)
The file was modified	`thys/Vickrey_Clarke_Groves/MiscTools.thy` (diff)
The file was modified	`thys/Vickrey_Clarke_Groves/StrictCombinatorialAuction.thy` (diff)
The file was modified	`thys/Vickrey_Clarke_Groves/UniformTieBreaking.thy` (diff)
The file was modified	`thys/Vickrey_Clarke_Groves/Universes.thy` (diff)
The file was modified	`thys/pGCL/Continuity.thy` (diff)
The file was modified	`thys/pGCL/Determinism.thy` (diff)
The file was modified	`thys/pGCL/Expectations.thy` (diff)
The file was modified	`thys/pGCL/Healthiness.thy` (diff)
The file was modified	`thys/pGCL/Misc.thy` (diff)
The file was modified	`thys/pGCL/StructuredReasoning.thy` (diff)
The file was modified	`thys/pGCL/Sublinearity.thy` (diff)
The file was modified	`thys/pGCL/Transformers.thy` (diff)
The file was modified	`thys/pGCL/Tutorial/Primitives.thy` (diff)
The file was modified	`thys/pGCL/WellDefined.thy` (diff)