Skip to content
[Jenkins]Jenkins
log in
Success

Changes

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

Summary

  1. merged
  2. added lemma monotone_on_o
  3. redefined mono_on and strict_mono_on as an abbreviation of monotone_on
  4. changed argument order of mono_on and strict_mono_on to uniformize with monotone_on and other predicates
Changeset 75610:da901dcafc29 by desharna:
merged
Changeset 75609:19ec8f844e08 by desharna:
added lemma monotone_on_o
The file was modified NEWS
The file was modified src/HOL/Fun.thy
Changeset 75608:6c542e152b8a by desharna:
redefined mono_on and strict_mono_on as an abbreviation of monotone_on
The file was modified NEWS
The file was modified src/HOL/Fun.thy
Changeset 75607:3c544d64c218 by desharna:
changed argument order of mono_on and strict_mono_on to uniformize with monotone_on and other predicates
The file was modified NEWS
The file was modified src/HOL/Analysis/Borel_Space.thy
The file was modified src/HOL/Analysis/Equivalence_Measurable_On_Borel.thy
The file was modified src/HOL/Fun.thy
The file was modified src/HOL/Hilbert_Choice.thy
The file was modified src/HOL/Library/Infinite_Set.thy
The file was modified src/HOL/Probability/Giry_Monad.thy
The file was modified src/HOL/Probability/Weak_Convergence.thy

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

Summary

  1. merged
  2. updated to Isabelle/3c544d64c218
Changeset 12727:0d159a7589cb by desharna:
merged
Changeset 12726:221e9df71dbb by desharna:
updated to Isabelle/3c544d64c218
The file was modified thys/Density_Compiler/PDF_Transformations.thy
The file was modified thys/Frequency_Moments/Frequency_Moment_0.thy
The file was modified thys/Frequency_Moments/K_Smallest.thy
The file was modified thys/Ordinal_Partitions/Erdos_Milner.thy
The file was modified thys/Ordinal_Partitions/Library_Additions.thy
The file was modified thys/Ordinal_Partitions/Omega_Omega.thy
The file was modified thys/Poincare_Bendixson/ODE_Misc.thy
The file was modified thys/Prime_Distribution_Elementary/Partial_Zeta_Bounds.thy
The file was modified thys/Prime_Distribution_Elementary/Prime_Distribution_Elementary_Library.thy
The file was modified thys/Prime_Distribution_Elementary/Primorial.thy
The file was modified thys/Random_BSTs/Random_BSTs.thy
The file was modified thys/Simplicial_complexes_and_boolean_functions/Bij_betw_simplicial_complex_bool_func.thy
The file was modified thys/Simplicial_complexes_and_boolean_functions/Boolean_functions.thy
The file was modified thys/Simplicial_complexes_and_boolean_functions/Simplicial_complex.thy
The file was modified thys/Skip_Lists/Misc.thy
The file was modified thys/Skip_Lists/Skip_List.thy
The file was modified thys/Smith_Normal_Form/Cauchy_Binet.thy
The file was modified thys/Smith_Normal_Form/SNF_Missing_Lemmas.thy
The file was modified thys/Smith_Normal_Form/SNF_Uniqueness.thy
The file was modified thys/Youngs_Inequality/Youngs.thy
The file was modified thys/ZFC_in_HOL/ZFC_Cardinals.thy
The file was modified thys/ZFC_in_HOL/ZFC_in_HOL.thy