Skip to content
Jenkins
log in
Dashboard
Thibault Dardinier <thibault.dardinier@inf.ethz.ch>
My Views
All
afp-repo
#414
Changes
Status
Changes
Console Output
View Build Information
Polling Log
Environment Variables
Mercurial Build Data
Embeddable Build Status
Previous Build
Next Build
Success
Changes
Summary
merged
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)