Skip to content
[Jenkins]Jenkins
log in
Failed

Changes

Changes from Mercurial (hg https://isabelle.in.tum.de/repos/isabelle/ default)

Summary

  1. Some new simprules – and patches for proofs
  2. merged
  3. merged
  4. A little more tidying in Nominal
Changeset 80175:200107cdd3ac by paulson _lp15@cam.ac.uk_:
Some new simprules – and patches for proofs
The file was modified src/HOL/Analysis/Arcwise_Connected.thy
The file was modified src/HOL/Analysis/Bochner_Integration.thy
The file was modified src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy
The file was modified src/HOL/Analysis/Further_Topology.thy
The file was modified src/HOL/Analysis/Henstock_Kurzweil_Integration.thy
The file was modified src/HOL/Analysis/Homeomorphism.thy
The file was modified src/HOL/Analysis/Kronecker_Approximation_Theorem.thy
The file was modified src/HOL/Analysis/Nonnegative_Lebesgue_Integration.thy
The file was modified src/HOL/Analysis/Starlike.thy
The file was modified src/HOL/Analysis/Weierstrass_Theorems.thy
The file was modified src/HOL/Binomial.thy
The file was modified src/HOL/Computational_Algebra/Formal_Laurent_Series.thy
The file was modified src/HOL/Computational_Algebra/Formal_Power_Series.thy
The file was modified src/HOL/Filter.thy
The file was modified src/HOL/HOLCF/Universal.thy
The file was modified src/HOL/Homology/Homology_Groups.thy
The file was modified src/HOL/Lattices_Big.thy
The file was modified src/HOL/Library/Landau_Symbols.thy
The file was modified src/HOL/Nat.thy
The file was modified src/HOL/NthRoot.thy
The file was modified src/HOL/Number_Theory/Quadratic_Reciprocity.thy
The file was modified src/HOL/Probability/Sinc_Integral.thy
The file was modified src/HOL/Random.thy
The file was modified src/HOL/Real_Asymp/Multiseries_Expansion.thy
The file was modified src/HOL/Transcendental.thy
The file was modified src/HOL/ex/HarmonicSeries.thy
Changeset 80174:32d2b96affc7 by paulson:
merged
Changeset 80173:8e486ad63579 by paulson:
merged
Changeset 80172:6c62605cb3f6 by paulson _lp15@cam.ac.uk_:
A little more tidying in Nominal
The file was modified src/HOL/Nominal/Examples/Class1.thy

Changes from Mercurial (hg https://foss.heptapod.net/isa-afp/afp-devel/ default)

Summary

  1. merged
  2. simprule status for of_nat_diff and eventually_frequently_const_simps; logical, caused quite a few incompatibilities
Changeset 14365:02484739ff7b by paulson:
merged
Changeset 14364:2a6a11b73760 by paulson _lp15@cam.ac.uk_:
simprule status for of_nat_diff and eventually_frequently_const_simps; logical, caused quite a few incompatibilities
The file was modified thys/Actuarial_Mathematics/Interest.thy
The file was modified thys/Amicable_Numbers/Amicable_Numbers.thy
The file was modified thys/Amortized_Complexity/Amortized_Examples.thy
The file was modified thys/Bernoulli/Bernoulli.thy
The file was modified thys/Card_Multisets/Card_Multisets.thy
The file was modified thys/Continued_Fractions/Sqrt_Nat_Cfrac.thy
The file was modified thys/CryptHOL/Cyclic_Group.thy
The file was modified thys/DPRM_Theorem/Diophantine/Exponentiation.thy
The file was modified thys/Decl_Sem_Fun_PL/DeclSemAsNDInterpFSet.thy
The file was modified thys/Decl_Sem_Fun_PL/DenotEqualitiesFSet.thy
The file was modified thys/Decl_Sem_Fun_PL/MutableRef.thy
The file was modified thys/Ergodic_Theory/Gouezel_Karlsson.thy
The file was modified thys/Ergodic_Theory/Invariants.thy
The file was modified thys/Ergodic_Theory/Kingman.thy
The file was modified thys/Falling_Factorial_Sum/Falling_Factorial_Sum_Induction.thy
The file was modified thys/Fishers_Inequality/Incidence_Matrices.thy
The file was modified thys/Fourier/Fourier.thy
The file was modified thys/Frequency_Moments/Frequency_Moment_k.thy
The file was modified thys/Groebner_Macaulay/Binomial_Int.thy
The file was modified thys/Groebner_Macaulay/Dube_Bound.thy
The file was modified thys/Group-Ring-Module/Algebra1.thy
The file was modified thys/Hahn_Jordan_Decomposition/Hahn_Jordan_Decomposition.thy
The file was modified thys/Hahn_Jordan_Decomposition/Hahn_Jordan_Prelims.thy
The file was modified thys/Hyperdual/Hyperdual.thy
The file was modified thys/Hypergraph_Colourings/Basic_Bounds_Application.thy
The file was modified thys/Hypergraph_Colourings/Hypergraph_Colourings_Root.thy
The file was modified thys/Hypergraph_Colourings/LLL_Applications.thy
The file was modified thys/Interval_Analysis/Lipschitz_Subdivisions_Refinements.thy
The file was modified thys/Jordan_Normal_Form/Jordan_Normal_Form.thy
The file was modified thys/Khovanskii_Theorem/Khovanskii.thy
The file was modified thys/Kneser_Cauchy_Davenport/Kneser_Cauchy_Davenport_main_proofs.thy
The file was modified thys/Laplace_Transform/Piecewise_Continuous.thy
The file was modified thys/List_Update/BIT.thy
The file was modified thys/List_Update/OPT2.thy
The file was modified thys/Lovasz_Local/Prob_Events_Extras.thy
The file was modified thys/MDP-Algorithms/Backward_Induction.thy
The file was modified thys/Markov_Models/Discrete_Time_Markov_Chain.thy
The file was modified thys/Nested_Multisets_Ordinals/McCarthy_91.thy
The file was modified thys/Parity_Game/WellOrderedStrategy.thy
The file was modified thys/Perron_Frobenius/Spectral_Radius_Largest_Jordan_Block.thy
The file was modified thys/Planarity_Certificates/Planarity/Graph_Genus.thy
The file was modified thys/Pluennecke_Ruzsa_Inequality/Pluennecke_Ruzsa_Inequality.thy
The file was modified thys/Polygonal_Number_Theorem/Polygonal_Number_Theorem_Cauchy.thy
The file was modified thys/Probabilistic_While/Fast_Dice_Roll.thy
The file was modified thys/Sigma_Commit_Crypto/Chaum_Pedersen_Sigma_Commit.thy
The file was modified thys/Sigma_Commit_Crypto/Schnorr_Sigma_Commit.thy
The file was modified thys/Skip_Lists/Skip_List.thy
The file was modified thys/Stirling_Formula/Gamma_Asymptotics.thy
The file was modified thys/Stirling_Formula/Stirling_Formula.thy
The file was modified thys/Subresultants/Subresultant.thy
The file was modified thys/Timed_Automata/Regions.thy
The file was modified thys/Turans_Graph_Theorem/Turan.thy
The file was modified thys/Undirected_Graph_Theory/Undirected_Graph_Basics.thy
The file was modified thys/Valuation/Valuation3.thy
The file was modified thys/Van_Emde_Boas_Trees/VEBT_Space.thy
The file was modified thys/X86_Semantics/Memory.thy
The file was modified thys/Zeta_3_Irrational/Zeta_3_Irrational.thy
The file was modified thys/Zeta_Function/Zeta_Function.thy