![[Jenkins]](/jenkins/static/77e8e0f1/images/svgs/logo.svg){kind=logo}
Summary
- add missing file Essential_Supremum.thy
- Merge
- Inserted necessary dependency
- suitable logical type class for abs, sgn
- HOL-Analysis: move Function Topology from AFP/Ergodict_Theory; HOL-Probability: move Essential Supremum from AFP/Lp
- Merge
- more from moretop.ml
- Jenkins: build in system mode again (backout of 3dbfd6758735)
- Jenkins: configurable clean build
- HOL-Analysis: more theorems from Sébastien Gouëzel's Ergodic_Theory
- HOL-Probability: move conditional expectation from AFP/Ergodic_Theory
- Removed Old_Number_Theory; all theories ported (thanks to Jaime Mendizabal Roche)
- restored document structure after theory refactoring
| The file was added | src/HOL/Probability/Essential_Supremum.thy |
| The file was modified | src/HOL/Analysis/Further_Topology.thy (diff) |
| The file was modified | NEWS (diff) |
| The file was modified | src/HOL/Complex.thy (diff) |
| The file was modified | src/HOL/Enum.thy (diff) |
| The file was modified | src/HOL/Fields.thy (diff) |
| The file was modified | src/HOL/Groups.thy (diff) |
| The file was modified | src/HOL/Library/Fraction_Field.thy (diff) |
| The file was modified | src/HOL/Nonstandard_Analysis/StarDef.thy (diff) |
| The file was modified | src/HOL/Quotient_Examples/Quotient_Rat.thy (diff) |
| The file was modified | src/HOL/Rings.thy (diff) |
| The file was added | src/HOL/Analysis/Function_Topology.thy |
| The file was added | src/HOL/Analysis/Further_Topology.thy |
| The file was modified | src/HOL/Analysis/Analysis.thy (diff) |
| The file was modified | src/HOL/Probability/Probability.thy (diff) |
| The file was removed | src/HOL/Analysis/FurtherTopology.thy |
| The file was modified | src/HOL/Analysis/Bochner_Integration.thy (diff) |
| The file was modified | src/HOL/Analysis/Borel_Space.thy (diff) |
| The file was modified | src/HOL/Analysis/Complex_Transcendental.thy (diff) |
| The file was modified | src/HOL/Analysis/Convex_Euclidean_Space.thy (diff) |
| The file was modified | src/HOL/Analysis/Derivative.thy (diff) |
| The file was modified | src/HOL/Analysis/FurtherTopology.thy (diff) |
| The file was modified | src/HOL/Analysis/Henstock_Kurzweil_Integration.thy (diff) |
| The file was modified | src/HOL/Analysis/Topology_Euclidean_Space.thy (diff) |
| The file was modified | src/HOL/Limits.thy (diff) |
| The file was modified | src/HOL/Orderings.thy (diff) |
| The file was modified | src/Pure/Admin/ci_profile.scala (diff) |
| The file was modified | src/Pure/Admin/ci_profile.scala (diff) |
| The file was modified | src/HOL/Analysis/Borel_Space.thy (diff) |
| The file was modified | src/HOL/Analysis/Complete_Measure.thy (diff) |
| The file was modified | src/HOL/Analysis/Set_Integral.thy (diff) |
| The file was modified | src/HOL/Analysis/Topology_Euclidean_Space.thy (diff) |
| The file was modified | src/HOL/Library/Extended_Nonnegative_Real.thy (diff) |
| The file was modified | src/HOL/Library/Permutations.thy (diff) |
| The file was modified | src/HOL/Probability/Levy.thy (diff) |
| The file was modified | src/HOL/Topological_Spaces.thy (diff) |
| The file was added | src/HOL/Probability/Conditional_Expectation.thy |
| The file was modified | src/HOL/Analysis/Bochner_Integration.thy (diff) |
| The file was modified | src/HOL/Analysis/Borel_Space.thy (diff) |
| The file was modified | src/HOL/Analysis/Measurable.thy (diff) |
| The file was modified | src/HOL/Analysis/Measure_Space.thy (diff) |
| The file was modified | src/HOL/Analysis/Nonnegative_Lebesgue_Integration.thy (diff) |
| The file was modified | src/HOL/Analysis/Radon_Nikodym.thy (diff) |
| The file was modified | src/HOL/Analysis/Set_Integral.thy (diff) |
| The file was modified | src/HOL/Probability/Characteristic_Functions.thy (diff) |
| The file was modified | src/HOL/Probability/Levy.thy (diff) |
| The file was modified | src/HOL/Probability/Probability.thy (diff) |
| The file was modified | src/HOL/Topological_Spaces.thy (diff) |
| The file was added | src/HOL/Number_Theory/Euler_Criterion.thy |
| The file was added | src/HOL/Number_Theory/QuadraticReciprocity.thy |
| The file was modified | src/HOL/Number_Theory/Gauss.thy (diff) |
| The file was modified | src/HOL/Number_Theory/Number_Theory.thy (diff) |
| The file was modified | src/HOL/Number_Theory/Pocklington.thy (diff) |
| The file was modified | src/HOL/Number_Theory/Residues.thy (diff) |
| The file was modified | src/HOL/ROOT (diff) |
| The file was removed | src/HOL/Old_Number_Theory/BijectionRel.thy |
| The file was removed | src/HOL/Old_Number_Theory/Chinese.thy |
| The file was removed | src/HOL/Old_Number_Theory/Euler.thy |
| The file was removed | src/HOL/Old_Number_Theory/EulerFermat.thy |
| The file was removed | src/HOL/Old_Number_Theory/EvenOdd.thy |
| The file was removed | src/HOL/Old_Number_Theory/Factorization.thy |
| The file was removed | src/HOL/Old_Number_Theory/Fib.thy |
| The file was removed | src/HOL/Old_Number_Theory/Finite2.thy |
| The file was removed | src/HOL/Old_Number_Theory/Gauss.thy |
| The file was removed | src/HOL/Old_Number_Theory/Int2.thy |
| The file was removed | src/HOL/Old_Number_Theory/IntFact.thy |
| The file was removed | src/HOL/Old_Number_Theory/IntPrimes.thy |
| The file was removed | src/HOL/Old_Number_Theory/Legacy_GCD.thy |
| The file was removed | src/HOL/Old_Number_Theory/Pocklington.thy |
| The file was removed | src/HOL/Old_Number_Theory/Primes.thy |
| The file was removed | src/HOL/Old_Number_Theory/Quadratic_Reciprocity.thy |
| The file was removed | src/HOL/Old_Number_Theory/Residues.thy |
| The file was removed | src/HOL/Old_Number_Theory/WilsonBij.thy |
| The file was removed | src/HOL/Old_Number_Theory/WilsonRuss.thy |
| The file was removed | src/HOL/Old_Number_Theory/document/root.bib |
| The file was removed | src/HOL/Old_Number_Theory/document/root.tex |
| The file was modified | src/Doc/Main/Main_Doc.thy (diff) |