Skip to content
[Jenkins]Jenkins
log in
Success

Changes

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 (diff)
The file was modified src/HOL/Fun.thy (diff)
Changeset 75608:6c542e152b8a by desharna:
redefined mono_on and strict_mono_on as an abbreviation of monotone_on
The file was modified NEWS (diff)
The file was modified src/HOL/Fun.thy (diff)
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 (diff)
The file was modified src/HOL/Analysis/Borel_Space.thy (diff)
The file was modified src/HOL/Analysis/Equivalence_Measurable_On_Borel.thy (diff)
The file was modified src/HOL/Fun.thy (diff)
The file was modified src/HOL/Hilbert_Choice.thy (diff)
The file was modified src/HOL/Library/Infinite_Set.thy (diff)
The file was modified src/HOL/Probability/Giry_Monad.thy (diff)
The file was modified src/HOL/Probability/Weak_Convergence.thy (diff)