Skip to content
Success

Changes

Summary

  1. added is_arg_min
  2. removed LeastM; is now arg_min
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)