Skip to content
[Jenkins]Jenkins
log in
Success

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