Skip to content
Jenkins
log in
Dashboard
afp-repo
#474
Changes
Status
Changes
Console Output
View Build Information
Polling Log
Timings
Environment Variables
Mercurial Build Data
Embeddable Build Status
Previous Build
Next Build
Failed
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)