Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. merged
  2. listsum/prod -> sum/prod_list
Changeset 7106:4a0af82f1147 by nipkow:
merged
Changeset 7105:003d55e9c3ce by nipkow:
listsum/prod -> sum/prod_list
The file was modified thys/Abstract-Rewriting/SN_Orders.thy (diff)
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/Intersection.thy (diff)
The file was modified thys/Affine_Arithmetic/Polygon.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/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/Complex_Algebraic_Numbers.thy (diff)
The file was modified thys/Algebraic_Numbers/Complex_Roots_Real_Poly.thy (diff)
The file was modified thys/Algebraic_Numbers/Real_Algebraic_Numbers.thy (diff)
The file was modified thys/Algebraic_Numbers/Real_Factorization.thy (diff)
The file was modified thys/Algebraic_Numbers/Resultant.thy (diff)
The file was modified thys/Amortized_Complexity/Amortized_Framework.thy (diff)
The file was modified thys/Amortized_Complexity/Pairing_Heap_List1_Analysis.thy (diff)
The file was modified thys/Binomial-Heaps/BinomialHeap.thy (diff)
The file was modified thys/Binomial-Heaps/SkewBinomialHeap.thy (diff)
The file was modified thys/Buildings/Algebra.thy (diff)
The file was modified thys/Buildings/Chamber.thy (diff)
The file was modified thys/Buildings/Coxeter.thy (diff)
The file was modified thys/Cauchy/CauchysMeanTheorem.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/Collections/GenCF/Impl/Impl_Array_Hash_Map.thy (diff)
The file was modified thys/Collections/ICF/gen_algo/PrioByAnnotatedList.thy (diff)
The file was modified thys/Collections/ICF/gen_algo/PrioUniqueByAnnotatedList.thy (diff)
The file was modified thys/Collections/ICF/impl/ArrayHashMap_Impl.thy (diff)
The file was modified thys/Collections/ICF/spec/AnnotatedListSpec.thy (diff)
The file was modified thys/Descartes_Sign_Rule/Descartes_Sign_Rule.thy (diff)
The file was modified thys/Dijkstra_Shortest_Path/Graph.thy (diff)
The file was modified thys/Echelon_Form/Code_Cayley_Hamilton.thy (diff)
The file was modified thys/Finger-Trees/FingerTree.thy (diff)
The file was modified thys/Formula_Derivatives/Presburger_Formula.thy (diff)
The file was modified thys/General-Triangle/GeneralTriangle.thy (diff)
The file was modified thys/Graph_Theory/Weighted_Graph.thy (diff)
The file was modified thys/JinjaThreads/Basic/Auxiliary.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/Determinant.thy (diff)
The file was modified thys/Jordan_Normal_Form/Determinant_Impl.thy (diff)
The file was modified thys/Jordan_Normal_Form/Jordan_Normal_Form.thy (diff)
The file was modified thys/Jordan_Normal_Form/Jordan_Normal_Form_Existence.thy (diff)
The file was modified thys/Jordan_Normal_Form/Jordan_Normal_Form_Uniqueness.thy (diff)
The file was modified thys/Jordan_Normal_Form/Matrix.thy (diff)
The file was modified thys/Jordan_Normal_Form/Matrix_Kernel.thy (diff)
The file was modified thys/Jordan_Normal_Form/Schur_Decomposition.thy (diff)
The file was modified thys/Landau_Symbols/Landau_Library.thy (diff)
The file was modified thys/Landau_Symbols/Landau_Real_Products.thy (diff)
The file was modified thys/List_Update/Move_to_Front.thy (diff)
The file was modified thys/Markov_Models/ex/MDP_RP_Certification.thy (diff)
The file was modified thys/Matrix/Matrix_Arith.thy (diff)
The file was modified thys/Matrix/Matrix_Comparison.thy (diff)
The file was modified thys/Matrix/Utility.thy (diff)
The file was modified thys/Multivariate_Polynomials/Poly_Lists.thy (diff)
The file was modified thys/NormByEval/NBE.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/Refine_Rigorous_Numerics.thy (diff)
The file was modified thys/Ordinary_Differential_Equations/Numerics/Refine_Rigorous_Numerics_Aform.thy (diff)
The file was modified thys/Ordinary_Differential_Equations/ODE_Auxiliarities.thy (diff)
The file was modified thys/Polynomial_Factorization/Berlekamp_Hensel_Factorization.thy (diff)
The file was modified thys/Polynomial_Factorization/Factorization_Oracle.thy (diff)
The file was modified thys/Polynomial_Factorization/Fundamental_Theorem_Algebra_Factorized.thy (diff)
The file was modified thys/Polynomial_Factorization/Kronecker_Factorization.thy (diff)
The file was modified thys/Polynomial_Factorization/Missing_List.thy (diff)
The file was modified thys/Polynomial_Factorization/Missing_Multiset.thy (diff)
The file was modified thys/Polynomial_Factorization/Polynomial_Divisibility.thy (diff)
The file was modified thys/Polynomial_Factorization/Prime_Factorization.thy (diff)
The file was modified thys/Polynomial_Factorization/Rational_Factorization.thy (diff)
The file was modified thys/Polynomial_Factorization/Square_Free_Factorization.thy (diff)
The file was modified thys/Polynomial_Interpolation/Lagrange_Interpolation.thy (diff)
The file was modified thys/Polynomial_Interpolation/Missing_Polynomial.thy (diff)
The file was modified thys/Polynomial_Interpolation/Missing_Unsorted.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/Polynomials/Polynomials.thy (diff)
The file was modified thys/Pratt_Certificate/Pratt_Certificate.thy (diff)
The file was modified thys/Presburger-Automata/Presburger_Automata.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/Language_Semantics.thy (diff)
The file was modified thys/QR_Decomposition/QR_Efficient.thy (diff)
The file was modified thys/Randomised_Social_Choice/Automation/SDS_Automation.thy (diff)
The file was modified thys/Randomised_Social_Choice/Automation/sds_automation.ML (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/Miscellaneous.thy (diff)
The file was modified thys/Rep_Fin_Groups/Rep_Fin_Groups.thy (diff)
The file was modified thys/Separation_Logic_Imperative_HOL/Examples/Hash_Map.thy (diff)
The file was modified thys/Separation_Logic_Imperative_HOL/Examples/Hash_Table.thy (diff)
The file was modified thys/Separation_Logic_Imperative_HOL/Examples/Idioms.thy (diff)
The file was modified thys/Separation_Logic_Imperative_HOL/Examples/Open_List.thy (diff)
The file was modified thys/Stream_Fusion_Code/Stream_Fusion_Examples.thy (diff)
The file was modified thys/Stream_Fusion_Code/Stream_Fusion_List.thy (diff)