Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. merged
  2. merged
  3. moved antimono to Fun and redefined it as an abbreviation
  4. moved mono and strict_mono to Fun and redefined them as abbreviations
Changeset 76057:e07d873c18a4 by desharna:
merged
Changeset 76056:c2fd8b88d262 by desharna:
merged
Changeset 76055:8d56461f85ec by desharna:
moved antimono to Fun and redefined it as an abbreviation
The file was modified NEWS (diff)
The file was modified src/Doc/Main/Main_Doc.thy (diff)
The file was modified src/HOL/Analysis/Nonnegative_Lebesgue_Integration.thy (diff)
The file was modified src/HOL/Fun.thy (diff)
The file was modified src/HOL/Lattices.thy (diff)
The file was modified src/HOL/Orderings.thy (diff)
The file was modified src/HOL/Real_Vector_Spaces.thy (diff)
Changeset 76054:a4b47c684445 by desharna:
moved mono and strict_mono to Fun and redefined them as abbreviations
The file was modified NEWS (diff)
The file was modified src/Doc/Main/Main_Doc.thy (diff)
The file was modified src/HOL/Fun.thy (diff)
The file was modified src/HOL/Groups.thy (diff)
The file was modified src/HOL/Lattices.thy (diff)
The file was modified src/HOL/Orderings.thy (diff)
The file was modified src/HOL/Set.thy (diff)
The file was modified src/HOL/Tools/inductive.ML (diff)