Skip to content
Success

Changes

Summary

  1. removed GreatestM
  2. introduced arg_max
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)