Summary
- removed GreatestM
- introduced arg_max
The file was modified | src/HOL/Hilbert_Choice.thy (diff) |
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) |