Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. removed GreatestM
  2. introduced arg_max
  3. added is_arg_min
  4. removed LeastM; is now arg_min
Changeset 65955:0616ba637b14 by nipkow:
removed GreatestM
The file was modified src/HOL/Hilbert_Choice.thy (diff)
Changeset 65954:431024edc9cf by nipkow:
introduced arg_max
The file was modified src/Doc/Main/Main_Doc.thy (diff)
The file was modified src/HOL/Hilbert_Choice.thy (diff)
The file was modified src/HOL/Lattices_Big.thy (diff)
The file was modified src/HOL/Library/Sublist.thy (diff)
Changeset 65953:440fe0937b92 by nipkow:
added is_arg_min
The file was modified src/Doc/Main/Main_Doc.thy (diff)
The file was modified src/Doc/Tutorial/Rules/Basic.thy (diff)
Changeset 65952:dec96cb3fbe0 by nipkow:
removed LeastM; is now arg_min
The file was modified src/Doc/Main/Main_Doc.thy (diff)
The file was modified src/HOL/Hilbert_Choice.thy (diff)
The file was modified src/HOL/Lattices_Big.thy (diff)